--- 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