--- 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)