diff options
Diffstat (limited to 'dev/doc/debugging.txt')
| -rw-r--r-- | dev/doc/debugging.txt | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index f0df2fc37..79cde4884 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -51,8 +51,8 @@ Debugging from Caml debugger failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle of each of error* functions or anomaly* functions in lib/util.ml - - If "source db" fails, recompile printers.cma with - "make dev/printers.cma" and try again + - If "source db" fails, do a "make printers" and try again (it should build + top_printers.cmo and the core cma files). Global gprof-based profiling ============================ |