# HG changeset patch
# User wenzelm
# Date 1590316984 -7200
# Node ID f5dd0abd49d11c148f9412ceae6afdd0480ba519
# Parent  ad063ac1f6170dd4f5915d0af3b4cdf3b1e8b4a1
clarified name;

diff -r ad063ac1f617 -r f5dd0abd49d1 etc/options
--- 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
diff -r ad063ac1f617 -r f5dd0abd49d1 src/Pure/Tools/build.scala
--- 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)