# HG changeset patch # User wenzelm # Date 1622842844 -7200 # Node ID 6f367240f09b1b6993a636d1c47c3640ee020703 # Parent b982362eeca436edaffb747659bbc96419e50d59 proper usage (amending f7ea394490f5); diff -r b982362eeca4 -r 6f367240f09b 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