etc/options
changeset 79948 8fe1ed4b5705
parent 79928 cdc87eed26c7
child 80246 245dd5f82462
--- a/etc/options	Thu Mar 21 13:05:49 2024 +0100
+++ b/etc/options	Thu Mar 21 16:35:55 2024 +0100
@@ -219,6 +219,9 @@
 option build_cluster_identifier : string = "build_cluster"
   -- "ISABELLE_IDENTIFIER for remote build cluster sessions"
 
+option build_benchmark_session : string = "FOLP-ex"
+  -- "representative benchmark session with short build time and requirements"
+
 option build_schedule : string = ""
   -- "path to pre-computed schedule"