changeset 36316 | f9b45eac4c60 |
parent 35022 | c844b93dd147 |
child 46967 | 499d9bbd8de9 |
--- a/lib/scripts/keywords Fri Apr 23 21:00:28 2010 +0200 +++ b/lib/scripts/keywords Fri Apr 23 22:39:49 2010 +0200 @@ -39,6 +39,7 @@ elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) { my $name = $1; my $kind = $2; + if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; } &set_keyword($name, $kind); } }