patch: 'Origin: vendor'
[debian/jabref.git] / debian / patches / 05_antlr32.patch
index c9bb3bb95dac7e1f01960ac2aab4d2775a265b5e..9e0aff7df8dcab1878d461fbcf6c269770ce6c10 100644 (file)
@@ -1085,14 +1085,14 @@ Last-Update: 2010-08-03
 -                int n_1 = list_identifier == null ? 0 : list_identifier.size();
 -                 
 -
--
--                for (int i_1=0; i_1<n_1; i_1++) {
--                    adaptor.addChild(root_1, list_identifier.get(i_1));
 +                while ( stream_identifier.hasNext() ) {
 +                    adaptor.addChild(root_1, stream_identifier.nextTree());
  
-                 }
+-                for (int i_1=0; i_1<n_1; i_1++) {
+-                    adaptor.addChild(root_1, list_identifier.get(i_1));
+-
 -                }
+                 }
 +                stream_identifier.reset();
  
                  adaptor.addChild(root_0, root_1);