diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-25 20:08:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-25 20:08:36 +0200 |
| commit | 83c3ee8659f1cee68909570fbf581a0e03233af7 (patch) | |
| tree | 3db33b7940b9ea8898180e219bb1639390882c93 /dev/doc | |
| parent | 6d4d16eb5518a9fb461e0f0433c9ce54d2197158 (diff) | |
| parent | c229958059b940f57238fb1c12868855419759ac (diff) | |
Merge PR #7290: Update debugging.md
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/debugging.md | 2 |
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 |