aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 61ebc9bbe..188d2d098 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2118,7 +2118,7 @@ let with_fail b f =
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed!")
| HasFailed msg ->
- if is_verbose () || !Flags.ide_slave then msg_info
+ if is_verbose () || !test_mode || !ide_slave then msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end