diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqmktop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index a9ec682209..88156f6fa4 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -316,6 +316,6 @@ let main () = clean main_file; raise reraise let retcode = - try Printexc.print main () with _ -> 1 + try Printexc.print main () with any -> 1 let _ = exit retcode |