aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide_main.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide_main.ml4')
-rw-r--r--ide/coqide_main.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 2dbb3f499..70c50e7ed 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -97,9 +97,9 @@ let () =
try
GtkThread.main ()
with
- | Sys.Break -> Minilib.prerr_endline "Interrupted."
+ | Sys.Break -> Minilib.log "Interrupted."
| e ->
- Minilib.safe_prerr_endline
+ Minilib.log
("CoqIde unexpected error:" ^ (Printexc.to_string e));
Coqide.crash_save 127
done