etc/options
changeset 71975 2d658beb815b
parent 71968 ec0ef3ebe75e
child 72071 d3cad9ecd0cc
--- a/etc/options	Sat Jun 20 21:44:43 2020 +0200
+++ b/etc/options	Sat Jun 20 22:35:24 2020 +0200
@@ -150,7 +150,7 @@
 
 section "PIDE Build"
 
-option pide_session : bool = false
+option pide_session : bool = true
   -- "build session heaps via PIDE"
 
 option pide_reports : bool = true