# 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; }