improved EVERY'
authoroheimb
Thu, 03 May 2001 18:22:36 +0200
changeset 11283 358f82c4550d
parent 11282 297a58ea405f
child 11284 981ea92a86dd
improved EVERY'
lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Thu May 03 17:51:29 2001 +0200
+++ b/lib/scripts/convert.pl	Thu May 03 18:22:36 2001 +0200
@@ -61,7 +61,7 @@
   s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
 
   s/EVERY *\[(.*?)\]/$1/;
-  if(s/EVERY\'\[(.*?)\] *(\d+)/$1 $2/) {
+  if(s/EVERY\' ?\[(.*?)\] *(\d+)/$1 $2/) {
     $goal = $2;
     s/,/ $goal,/g;
   }