etc/options

--- a/etc/options	Thu Jun 18 09:07:54 2020 +0000
+++ b/etc/options	Fri Jun 19 16:12:32 2020 +0200
@@ -153,6 +153,9 @@
 option pide_session : bool = true
   -- "build session heaps via PIDE"
 
+option pide_exports : bool = true
+  -- "store PIDE export artifacts"
+
 option pide_reports : bool = true
   -- "report PIDE markup"