From 7d8389d012aa8dbdeb7b82217087f1b7dfb2b24e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 9 Sep 2020 02:07:44 -0700
Subject: Add additional escape sequences for notations

---
 doc/tools/docgram/doc_grammar.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/tools/docgram')

diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 96eaff2895..548ca7364c 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -309,6 +309,11 @@ let rec output_prodn = function
             | "{|" -> "%{%|"
             | "`{" -> "`%{"
             | "@{" -> "@%{"
+            | "|-" -> "%|-"
+            | "|->" -> "%|->"
+            | "||" -> "%||"
+            | "|||" -> "%|||"
+            | "||||" -> "%||||"
             | "{"
             | "}"
             | "|" -> "%" ^ s
-- 
cgit v1.2.3