aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3936d2e80..2bc4fa97c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -123,8 +123,8 @@ let compile_files () =
let set_compat_version = function
| "8.3" -> compat_version := Some V8_3
| "8.2" -> compat_version := Some V8_2
- | "8.1" -> warning "Compatibility with version 8.1 not supported."
- | "8.0" -> warning "Compatibility with version 8.0 not supported."
+ | "8.1" -> msg_warning (str "Compatibility with version 8.1 not supported.")
+ | "8.0" -> msg_warning (str "Compatibility with version 8.0 not supported.")
| s -> error ("Unknown compatibility version \""^s^"\".")
(*s options for the virtual machine *)