aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/usage.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8f77aea44..de41f7b19 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -82,7 +82,7 @@ let print_usage_channel co command =
\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
\n stdout (if unset)\
\n -time display the time taken by each command\
-\n -profile-ltac display the time taken by each (sub)tactic\
+\n -profile-ltac display the time taken by each (sub)tactic\
\n -m, --memory display total heap size at program exit\
\n (use environment variable\
\n OCAML_GC_STATS=\"/tmp/gclog.txt\"\