allowing indentation of 'theory' keyword
authorhaftmann
Tue, 08 Nov 2005 15:26:35 +0100
changeset 18125 50e63c68768f
parent 18124 a310c78298f9
child 18126 b74145e46e0d
allowing indentation of 'theory' keyword
lib/scripts/fixheaders.pl
--- a/lib/scripts/fixheaders.pl	Tue Nov 08 10:44:40 2005 +0100
+++ b/lib/scripts/fixheaders.pl	Tue Nov 08 15:26:35 2005 +0100
@@ -24,9 +24,9 @@
     close ISTREAM or die $!;
     my $content = join("", @content);
     $_ = $content;
-    if (m!^theory!cgoms) {
+    if (m!^(\s*theory)!cgoms) {
         my $prelude = $`;
-        my $thyheader = "theory";
+        my $thyheader = $1;
         $thyheader .= skip_wscomment();
         if (m!\G(\S+)!cgoms) {
             $thyheader .= $1;