aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-08-29 14:09:03 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-08-29 14:09:03 -0400
commit75ca099bc54bd35c10e554996b8660f708642b14 (patch)
tree8e4ac22f1dcc0de404705e2ef207505516d612f3 /dev/doc
parentd1c64c9e74604d08541070f70537d80f7d49d345 (diff)
mention issue with OCAMLRUNPARAM and ocamldebug
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/debugging.txt3
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 3e2b435b3..86e0f0470 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -53,6 +53,9 @@ Debugging from Caml debugger
of each of error* functions or anomaly* functions in lib/util.ml
- If "source db" fails, do a "make printers" and try again (it should build
top_printers.cmo and the core cma files).
+ - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on
+ startup when run from the debugger. If this happens, unset the variable,
+ re-start Emacs, and run the debugger again.
Global gprof-based profiling
============================