clarified name;
authorwenzelm
Sun May 24 12:43:04 2020 +0200 (6 weeks ago)
changeset 71877f5dd0abd49d1
parent 71876 ad063ac1f617
child 71878 3cd8449829fa
clarified name;
etc/options
src/Pure/Tools/build.scala
     1.1 --- a/etc/options	Sun May 24 12:38:41 2020 +0200
     1.2 +++ b/etc/options	Sun May 24 12:43:04 2020 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4  
     1.5  section "PIDE Build"
     1.6  
     1.7 -option pide_build : bool = false
     1.8 +option pide_session : bool = false
     1.9    -- "build session heaps via PIDE"
    1.10  
    1.11  option pide_reports : bool = true
     2.1 --- a/src/Pure/Tools/build.scala	Sun May 24 12:38:41 2020 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sun May 24 12:43:04 2020 +0200
     2.3 @@ -216,7 +216,7 @@
     2.4            }
     2.5            else Nil
     2.6  
     2.7 -        if (options.bool("pide_build")) {
     2.8 +        if (options.bool("pide_session")) {
     2.9            val resources = new Resources(sessions_structure, deps(parent))
    2.10            val session = new Session(options, resources)
    2.11