Commit def0a5f9 authored by François Bobot's avatar François Bobot

longlines (rq: Is it normal to add extra_options for the command *editor*?)

parent 0d74654a
......@@ -395,9 +395,12 @@ loaded@."
end
in
set_timelimit timelimit a;
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt
~timelimit ~memlimit:0
?old ~command:(String.concat " " (npc.prover_config.Whyconf.command :: npc.prover_config.Whyconf.extra_options))
?old ~command
~driver:npc.prover_driver
~callback
eT
......@@ -627,9 +630,12 @@ let check_external_proof eS eT todo a =
(* Format.eprintf "Info: proving using edited file %s@." f; *)
(Some (open_in f))
in
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt eT
~timelimit:a.proof_timelimit ~memlimit:0
?old ~command:(String.concat " " (npc.prover_config.Whyconf.command :: npc.prover_config.Whyconf.extra_options))
?old ~command
~driver:npc.prover_driver
~callback
(goal_task g)
......@@ -755,7 +761,8 @@ let edit_proof eS sched ~default_editor a =
let editor =
match npc.prover_config.Whyconf.editor with
| "" -> default_editor
| s -> String.concat " " (s :: npc.prover_config.Whyconf.extra_options)
| s ->
String.concat " "(s :: npc.prover_config.Whyconf.extra_options)
in
(*
eprintf "[Editing] goal %s with command %s %s@."
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment