- MatitaLog.message
- (sprintf "execution of %s completed in %s." fname (hou^min^sec))) scripts;
- Http_getter.sync_dump_file ();
- exit(0)
-
-
+ let proof_status = status.proof_status in
+ if proof_status <> MatitaTypes.No_proof then
+ begin
+ MatitaLog.error
+ "there are still incomplete proofs at the end of the script";
+ exit(-1)
+ end
+ else
+ begin
+ MatitaLog.message
+ (sprintf "execution of %s completed in %s." fname (hou^min^sec)) ;
+ exit(0)
+ end
+ ) scripts
+ with Sys.Break ->
+ MatitaLog.error "user break!";
+ exit (-1)