etc/options
changeset 71877 f5dd0abd49d1
parent 71845 b8d7b623e274
child 71940 026de3424c39
--- 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