# HG changeset patch
# User wenzelm
# Date 1622838617 -7200
# Node ID e67c951f1c186a06cac7e058a255b980eb6548ea
# Parent  4addb970720053cae31851477ccdc673be433ce2
removed pointless option (see 3d0952893db8);

diff -r 4addb9707200 -r e67c951f1c18 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jun 04 22:01:16 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Jun 04 22:30:17 2021 +0200
@@ -161,7 +161,6 @@
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var output_dir = default_output_dir
-    var requirements = false
     var theories: List[String] = Nil
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
@@ -183,7 +182,6 @@
     -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 + """,
-    -R           refer to requirements of selected sessions
     -T THEORY    theory restriction: NAME or NAME[LINE:END_LINE]
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
@@ -213,7 +211,6 @@
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "O:" -> (arg => output_dir = Path.explode(arg)),
-      "R" -> (_ => requirements = true),
       "T:" -> (arg => theories = theories ::: List(arg)),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
@@ -241,7 +238,6 @@
         mirabelle(options, actions, output_dir,
           theories = theories,
           selection = Sessions.Selection(
-            requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,