# HG changeset patch
# User wenzelm
# Date 1492950442 -7200
# Node ID a04afc400156c3d68a91aeeeae51426ad7da25b0
# Parent  006a274cdbc2140a4be4112165822dd4f6423b6f
prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);

diff -r 006a274cdbc2 -r a04afc400156 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 14:15:09 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 14:27:22 2017 +0200
@@ -73,11 +73,8 @@
     val options = this.options.value
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
-      try {
-        Sessions.session_base(
-          options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
-      }
-      catch { case ERROR(_) => Sessions.Base.pure(options) }
+      Sessions.session_base(
+        options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
 
     _resources = new JEdit_Resources(session_base.platform_path)
   }