From d35a5022f45f1082c83891a6d0af32485a9db7d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 25 Feb 2014 17:04:51 +0100
Subject: Fixing printing of only_parsing notations.

---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3