Commit 92cb6ec2 authored by MARCHE Claude's avatar MARCHE Claude

fix pb with time limit

parent db3b3780
......@@ -429,8 +429,12 @@ let set_proof_state ~obsolete a =
Format.sprintf "%.2f [%d.0]" time a.M.timelimit
else
Format.sprintf "%.2f" time
| Session.Unedited -> "not yet edited"
| _ -> ""
| Session.Unedited -> "(not yet edited, edit with \"Edit\" button)"
| Session.InternalFailure _ -> "(internal failure)"
| Session.Interrupted -> "(interrupted)"
| Session.Scheduled | Session.Running ->
Format.sprintf "[limit=%d.0]" a.M.timelimit
| Session.Undone -> "(undone)"
in
let t = if obsolete then t ^ " (obsolete)" else t in
goals_model#set ~row:row#iter ~column:time_column t
......
......@@ -1574,6 +1574,7 @@ let redo_external_proof ~timelimit g a =
(Some (open_in f))
end
in
a.timelimit <- timelimit;
schedule_proof_attempt
~debug:false ~timelimit ~memlimit:0
?old ~command:p.command ~driver:p.driver
......
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