aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 13:54:13 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 13:54:13 +0000
commitd73bf48c107e7f3e08f2fc5777bbbd42b4e1bc7c (patch)
treeef18d6e605c3f98392a226a2d3df68a1d0b0481c /toplevel/coqinit.ml
parent8d77cb907a3595c90f15e1aa6402868ad4e43242 (diff)
Added backtrace information to anomalies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 59d73e7bd..b4d0bc413 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -11,7 +11,9 @@ open Pp
let (/) = Filename.concat
-let set_debug () = Flags.debug := true
+let set_debug () =
+ let () = Printexc.record_backtrace true in
+ Flags.debug := true
(* Loading of the ressource file.
rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one