Commit d457ce5a authored by MARCHE Claude's avatar MARCHE Claude

Clean should also remove interrupted proofs

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