From 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Sep 2014 16:57:59 +0200 Subject: Undo prints only if coqtop || emacs --- toplevel/coqtop.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3eee9658e..3525d93c6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -250,6 +250,11 @@ let get_async_proofs_mode opt = function | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 +let get_cache opt = function + | "force" -> Some Flags.Force + | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + + let set_worker_id opt s = assert (s <> "master"); Flags.async_proofs_worker_id := s @@ -373,6 +378,8 @@ let parse_args arglist = Flags.async_proofs_mode := get_async_proofs_mode opt (next()) |"-async-proofs-j" -> Flags.async_proofs_n_workers := (get_int opt (next ())) + |"-async-proofs-cache" -> + Flags.async_proofs_cache := get_cache opt (next ()) |"-async-proofs-tac-j" -> Flags.async_proofs_n_tacworkers := (get_int opt (next ())) |"-async-proofs-worker-priority" -> -- cgit v1.2.3