Commit 4daca603 authored by MARCHE Claude's avatar MARCHE Claude Committed by Guillaume Melquiond
Browse files

Clean should also remove interrupted proofs

parent 7e5591a3
...@@ -905,9 +905,10 @@ let remove_metas t = ...@@ -905,9 +905,10 @@ let remove_metas t =
*) *)
let proof_removable a = let proof_removable a =
match a.proof_state with match a.proof_state with
| Scheduled | Running -> false
| Done pr -> | Done pr ->
a.proof_obsolete || pr.Call_provers.pr_answer <> Call_provers.Valid a.proof_obsolete || pr.Call_provers.pr_answer <> Call_provers.Valid
| _ -> false | Unedited | JustEdited | Interrupted | InternalFailure _ -> true
let rec clean = function let rec clean = function
......
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