fixed malconfigured option output_dir in mirabelle
authordesharna
Tue, 03 Aug 2021 10:33:35 +0200
changeset 74379 5cd8b5cd0451
parent 74378 58e208ad4bcf
child 74380 30ab39ab4117
fixed malconfigured option output_dir in mirabelle
src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Aug 04 08:27:16 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Aug 03 10:33:35 2021 +0200
@@ -62,7 +62,9 @@
       val build_options =
         options + "timeout_build=false" +
           ("mirabelle_actions=" + actions.mkString(";")) +
-          ("mirabelle_theories=" + theories.mkString(","))
+          ("mirabelle_theories=" + theories.mkString(",")) +
+          ("mirabelle_output_dir=" + output_dir.implode)
+
 
       progress.echo("Running Mirabelle ...")
 
@@ -192,8 +194,6 @@
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
-    options = options + ("mirabelle_output_dir=" + output_dir.implode)
-
     val sessions = getopts(args)
     if (actions.isEmpty) getopts.usage()
 
@@ -207,7 +207,7 @@
 
     val results =
       progress.interrupt_handler {
-        mirabelle(options, actions, output_dir,
+        mirabelle(options, actions, output_dir.absolute,
           theories = theories,
           selection = Sessions.Selection(
             all_sessions = all_sessions,