aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
authorJim Fehrle2020-09-27 00:49:28 -0700
committerJim Fehrle2020-10-04 09:29:22 -0700
commit5b194f6c4f16b99fe8ebe3c8004c31c01aec0b3b (patch)
tree1f7d6b6c37d7a53e7a68b978f6c19cdf9e0c7526 /doc/tools
parent9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff)
Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/docgram/fullGrammar1
-rw-r--r--doc/tools/docgram/orderedGrammar1
2 files changed, 0 insertions, 2 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..328175e65c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1761,7 +1761,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..6ae99880b3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1268,7 +1268,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)