aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-06 16:12:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-06 16:55:35 +0100
commitb4b315107cdf15c1358512c78ebbb5b2c19e8455 (patch)
tree7fa106d8a277834ecdac93cdb2c4852fb5c13fac /lib/future.ml
parent183a35d7b6eaaa377ecda21d32b3bf183ecea9dd (diff)
fix typo
Diffstat (limited to 'lib/future.ml')
-rw-r--r--lib/future.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/future.ml b/lib/future.ml
index 191fc3fdd..b6cb498c6 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -22,7 +22,7 @@ let _ = Errors.register_handler (function
| NotHere ->
Pp.strbrk("The value you are asking for is not available "^
"in this process. If you really need this, pass "^
- "the \"-async-proofs off\" option to CoqIDE to disable"^
+ "the \"-async-proofs off\" option to CoqIDE to disable "^
"asynchronous script processing.")
| _ -> raise Errors.Unhandled)