aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorHugo Herbelin2019-01-06 19:40:04 +0100
committerVincent Laporte2019-03-19 08:40:21 +0000
commit25cbf4cefa2102b11c3617c0c52f67d98fbffaac (patch)
tree500068650d3225a4f90a965aa2ae2178666600d9 /ide
parent68c1261978639a6a8e8467294fb6eaf3d70a2234 (diff)
CoqIDE: More informative message when failing editing/saving preferences.
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2f2478372e..49ff53eda1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -213,7 +213,8 @@ let check_save ?parent ~saveas sn =
exception DontQuit
let check_quit ?parent saveall =
- (try save_pref () with _ -> flash_info "Cannot save preferences");
+ (try save_pref ()
+ with e -> flash_info ("Cannot save preferences (" ^ Printexc.to_string e ^ ")"));
let is_modified sn = sn.buffer#modified in
if List.exists is_modified notebook#pages then begin
let answ = Configwin_ihm.question_box ~title:"Quit"
@@ -1021,7 +1022,8 @@ let build_ui () =
~callback:(fun _ ->
begin
try Preferences.configure ~apply:refresh_notebook_pos w
- with _ -> flash_info "Cannot save preferences"
+ with e ->
+ flash_info ("Editing preferences failed (" ^ Printexc.to_string e ^ ")")
end;
reset_revert_timer ());
];