Backport PR coq#17495: Remove leftover "redoing byextend" debug message

Zimmi48 · May 16, 2023 · bce0c29 · bce0c29
2 parents 7c7041d + d3a22f2
commit bce0c29
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/doc/changelog/13-misc/17495-byextendmsg.rst b/doc/changelog/13-misc/17495-byextendmsg.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  an impossible to turn off debug message "backtracking and redoing byextend on ..."
+  (`#17495 <https://github.com/coq/coq/pull/17495>`_,
+  fixes `#17488 <https://github.com/coq/coq/issues/17488>`_,
+  by Gaëtan Gilbert).
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
@@ -165,7 +165,6 @@ let rec remove_grammars n =
          camlp5_state := t;
          remove_grammars (n-1)
        | ByEXTEND (name, undo,redo)::t ->
-         Feedback.msg_info Pp.(str "backtracking and redoing byextend on " ++ str name);
            undo();
            camlp5_state := t;
            remove_grammars n;