--- a/etc/options Thu Aug 06 17:51:37 2020 +0200
+++ b/etc/options Thu Aug 06 22:43:40 2020 +0200
@@ -150,9 +150,6 @@
section "PIDE Build"
-option pide_session : bool = true
- -- "build session heaps via PIDE"
-
option pide_reports : bool = true
-- "report PIDE markup"