diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 16:57:59 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 17:34:57 +0200 |
| commit | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch) | |
| tree | 2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /toplevel | |
| parent | 26aa224293e88611dcb543e400488013bc8b30b4 (diff) | |
Undo prints only if coqtop || emacs
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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" -> |