diff --git a/collects/errortrace/doc.txt b/collects/errortrace/doc.txt index dd5fb57ea3..1c3dd5d31d 100644 --- a/collects/errortrace/doc.txt +++ b/collects/errortrace/doc.txt @@ -155,6 +155,10 @@ Gets the current profile results and displays them. It optionally shows paths information (if it is recorded) and sorts by either time or call counts. +> (clear-profile-results) + +Clears accumulated profile results. + Coverage --------