etc/options
changeset 71962 23398ed3aecf
parent 71960 6a64205b491a
child 71968 ec0ef3ebe75e
--- a/etc/options	Fri Jun 19 18:22:03 2020 +0200
+++ b/etc/options	Fri Jun 19 18:29:37 2020 +0200
@@ -150,7 +150,7 @@
 
 section "PIDE Build"
 
-option pide_session : bool = true
+option pide_session : bool = false
   -- "build session heaps via PIDE"
 
 option pide_exports : bool = true