# HG changeset patch
# User wenzelm
# Date 1693220424 -7200
# Node ID b96b73a79da3a40dbe228cdd06be68dcde21c73a
# Parent  dccfe13878a53edf691d142d32f0c01ddf7d9649
more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);

diff -r dccfe13878a5 -r b96b73a79da3 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Aug 27 19:07:12 2023 +0200
+++ b/lib/scripts/getsettings	Mon Aug 28 13:00:24 2023 +0200
@@ -78,7 +78,7 @@
 
 ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
 
-ISABELLE_HOSTNAME="$(hostname -s)"
+ISABELLE_HOSTNAME="$(hostname -s 2>/dev/null || uname -n)"
 
 
 # components