fix double-@ in Prelude code
authorSimon Marlow <marlowsd@gmail.com>
Wed, 14 Jul 2010 09:52:29 +0000 (09:52 +0000)
committerSimon Marlow <marlowsd@gmail.com>
Wed, 14 Jul 2010 09:52:29 +0000 (09:52 +0000)
tools/splitAndIndexPgm

index 809585d..c81dfb4 100644 (file)
@@ -34,7 +34,6 @@ while ($ARGV[0] =~ /^-/) {
 print "\\noindent\\bprogB\n\@\n";
 while (<>) {
     $currState = &newState();
-    s/@/@@/g; # for verbatim...
 
     if ($prevState eq 'blankLine' &&
        ($currState =~ /^toplev/)) { # a break OK here