clarified name;
authorwenzelm
Sun, 24 May 2020 12:43:04 +0200
changeset 71877 f5dd0abd49d1
parent 71876 ad063ac1f617
child 71878 3cd8449829fa
clarified name;
etc/options
src/Pure/Tools/build.scala
--- a/etc/options	Sun May 24 12:38:41 2020 +0200
+++ b/etc/options	Sun May 24 12:43:04 2020 +0200
@@ -150,7 +150,7 @@
 
 section "PIDE Build"
 
-option pide_build : bool = false
+option pide_session : bool = false
   -- "build session heaps via PIDE"
 
 option pide_reports : bool = true
--- a/src/Pure/Tools/build.scala	Sun May 24 12:38:41 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 24 12:43:04 2020 +0200
@@ -216,7 +216,7 @@
           }
           else Nil
 
-        if (options.bool("pide_build")) {
+        if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)