# HG changeset patch
# User oheimb
# Date 988906956 -7200
# Node ID 358f82c4550d805225190abd825a81b0a3d97560
# Parent  297a58ea405f76e1b8bec5f907b94b1170084b9b
improved EVERY'

diff -r 297a58ea405f -r 358f82c4550d 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;
   }