From 797eb524853e361f84c9c776024c142107f0c282 Mon Sep 17 00:00:00 2001
From: charguer
Date: Thu, 12 Dec 2019 10:48:50 +0100
Subject: Fix #11195 and add other improvements: try loading .vio (and not just
 .vo) if the .vos file is empty, rename -quick to -vio, dump empty .vos when
 producing .vio, dump empty .vos and .vok files when producing .vo from .vio.

---
 lib/future.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/future.ml b/lib/future.ml
index d3ea538549..5cccd2038d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -12,13 +12,13 @@ let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing and don't pass \"-quick\" to "^
+                "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))
 let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing and don't pass \"-quick\" to "^
+                "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))
 
 let customize_not_ready_msg f = not_ready_msg := f
-- 
cgit v1.2.3