aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/common.edit_mlg
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
-rw-r--r--doc/tools/docgram/common.edit_mlg1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index b932fc6e30..48d399dfd3 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
| REPLACE term99 ":" term200
| WITH term99 ":" type
| MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
]
constr: [