permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;

--- a/src/Pure/System/isabelle_system.ML	Tue Sep 21 00:20:55 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Sep 21 11:23:18 2021 +0200
@@ -180,6 +180,7 @@
 
 fun isabelle_name () = getenv_strict "ISABELLE_NAME";
 
-fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
+fun identification () =
+  "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading ();
 
 end;

--- a/src/Pure/System/isabelle_system.scala	Tue Sep 21 00:20:55 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 21 11:23:18 2021 +0200
@@ -139,7 +139,8 @@
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
-  def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
+  def identification(): String =
+    "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
 
 
   /** file-system operations **/