diff --git a/tools/gram.sed b/tools/gram.sed index 79e2b821d0..3773119f1a 100644 --- a/tools/gram.sed +++ b/tools/gram.sed @@ -2,13 +2,13 @@ /^%gram:/s/^%gram:[[:space:]]*//p # copy bnftab groups: -/^\\begin{bnftab}/,/^\\end{bnftab}/p +/^\\begin\{bnftab}/,/^\\end\{bnftab}/p # copy simplebnf groups: -/^\\begin{simplebnf}/,/^\\end{simplebnf}/p +/^\\begin\{simplebnf}/,/^\\end\{simplebnf}/p # copy bnf groups: -/^\\begin{bnf}/,/^\\end{bnf}/p +/^\\begin\{bnf}/,/^\\end\{bnf}/p # copy bnfkeywordtab groups: -/^\\begin{bnfkeywordtab}/,/^\\end{bnfkeywordtab}/p +/^\\begin\{bnfkeywordtab}/,/^\\end\{bnfkeywordtab}/p diff --git a/tools/gramb.sed b/tools/gramb.sed index 0a511a61c2..878e72e273 100644 --- a/tools/gramb.sed +++ b/tools/gramb.sed @@ -1,9 +1,9 @@ # copy bnftab groups: -/^\\end{bnftab}/a\ +/^\\end\{bnftab}/a\ # copy simplebnf groups: -/^\\end{simplebnf}/a\ +/^\\end\{simplebnf}/a\ # copy bnf groups: -/^\\end{bnf}/a\ +/^\\end\{bnf}/a\ diff --git a/tools/makegram b/tools/makegram old mode 100644 new mode 100755 diff --git a/tools/maketags b/tools/maketags old mode 100644 new mode 100755 diff --git a/tools/makexref b/tools/makexref old mode 100644 new mode 100755