aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/metasyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0aec4a7b72..58f8d6d4e5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -934,7 +934,7 @@ let is_not_printable onlyparse noninjective = function
if not onlyparse && noninjective then
let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
true
- else false
+ else onlyparse
let find_precedence lev etyps symbols =
match symbols with