aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-04-15 15:29:56 -0700
committerGravatar GitHub <noreply@github.com>2018-04-15 15:29:56 -0700
commitc229958059b940f57238fb1c12868855419759ac (patch)
treef94798e218026eb5e4567b85538dd0b25561b620 /dev/doc
parent4c466c429902d0ef0bd0da0f42e1a3b6d9f7d32a (diff)
Update debugging.md
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/debugging.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fd3cbd1bc..14a1cc693 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs
7. some hints:
- To debug a failure/error/anomaly, add a breakpoint in
- Vernac.vernac_com at the with clause of the "try ... interp com
+ `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
with ..." block, then go "back" a few steps to find where the
failure/error/anomaly has been raised
- Alternatively, for an error or an anomaly, add breakpoints in the middle