proper usage (amending f7ea394490f5);
authorwenzelm
Fri, 04 Jun 2021 23:40:44 +0200
changeset 73807 6f367240f09b
parent 73806 b982362eeca4
child 73808 da3405e5cd58
proper usage (amending f7ea394490f5);
src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jun 04 23:37:27 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jun 04 23:40:44 2021 +0200
@@ -182,7 +182,7 @@
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
-    -O DIR       output directory for log files (default: """ + default_output_dir + """,
+    -O DIR       output directory for log files (default: """ + default_output_dir + """)
     -T THEORY    theory restriction: NAME or NAME[LINE:END_LINE]
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions