# HG changeset patch
# User wenzelm
# Date 1572987629 -3600
# Node ID b64fc38327aeb57502de9508d7a5db065c674b3c
# Parent  ba14aa0b5a5d9610b3967dd4732b91fb48f29855
prefer system user setup, e.g. avoid occurrence on login screen;

diff -r ba14aa0b5a5d -r b64fc38327ae src/Pure/System/linux.scala
--- a/src/Pure/System/linux.scala	Tue Nov 05 21:43:51 2019 +0100
+++ b/src/Pure/System/linux.scala	Tue Nov 05 22:00:29 2019 +0100
@@ -83,7 +83,10 @@
 
   def user_home(name: String): String = user_entry(name, 6)
 
-  def user_add(name: String, description: String = "", ssh_setup: Boolean = false)
+  def user_add(name: String,
+    description: String = "",
+    system: Boolean = false,
+    ssh_setup: Boolean = false)
   {
     require(!description.contains(','))
 
@@ -91,6 +94,7 @@
 
     Isabelle_System.bash(
       "adduser --quiet --disabled-password --gecos " + Bash.string(description) +
+        (if (system) " --system --group --shell /bin/bash " else "") +
         " " + Bash.string(name)).check
 
     if (ssh_setup) {
diff -r ba14aa0b5a5d -r b64fc38327ae src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Nov 05 21:43:51 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Tue Nov 05 22:00:29 2019 +0100
@@ -99,7 +99,7 @@
   def user_setup(name: String, description: String, ssh_setup: Boolean = false)
   {
     if (!Linux.user_exists(name)) {
-      Linux.user_add(name, description = description, ssh_setup = ssh_setup)
+      Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
     }
     else if (Linux.user_description(name) != description) {
       error("User " + quote(name) + " already exists --" +