# HG changeset patch
# User wenzelm
# Date 1592643717 -7200
# Node ID ec0ef3ebe75ec46e7ee8a57f6ae3c075597d8b14
# Parent  65ad3a6cee815b0c719caddf4036f8cd0e00302d
removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);

diff -r 65ad3a6cee81 -r ec0ef3ebe75e etc/options
--- a/etc/options	Fri Jun 19 20:15:00 2020 +0200
+++ b/etc/options	Sat Jun 20 11:01:57 2020 +0200
@@ -153,9 +153,6 @@
 option pide_session : bool = false
   -- "build session heaps via PIDE"
 
-option pide_exports : bool = true
-  -- "store PIDE export artifacts"
-
 option pide_reports : bool = true
   -- "report PIDE markup"
 
diff -r 65ad3a6cee81 -r ec0ef3ebe75e src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Jun 19 20:15:00 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Jun 20 11:01:57 2020 +0200
@@ -501,11 +501,9 @@
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
-                if (session_options.bool("pide_exports")) {
-                  val id = Value.Long.unapply(args.id.get).get
-                  val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
-                  change_command(_.add_export(id, (args.serial, export)))
-                }
+                val id = Value.Long.unapply(args.id.get).get
+                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                change_command(_.add_export(id, (args.serial, export)))
 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
diff -r 65ad3a6cee81 -r ec0ef3ebe75e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jun 19 20:15:00 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 20 11:01:57 2020 +0200
@@ -492,7 +492,6 @@
         "ML_statistics" +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
-        "pide_exports=false" +
         "pide_reports=false"
 
     val store = Sessions.store(build_options)