# HG changeset patch # User wenzelm # Date 1573731726 -3600 # Node ID 30ed6786d775f20c03d1f0822c1311d9af59583a # Parent 2bc568573a47fc47a3e8c6f88cdb9486c7e524e4 more portable; diff -r 2bc568573a47 -r 30ed6786d775 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Nov 14 11:49:54 2019 +0100 +++ b/src/Pure/System/isabelle_system.scala Thu Nov 14 12:42:06 2019 +0100 @@ -152,10 +152,10 @@ /* permissions */ def chmod(arg: String, path: Path): Unit = - bash("chmod " + Bash.string(arg) + " -- " + File.bash_path(path)).check + bash("chmod " + Bash.string(arg) + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = - bash("chown " + Bash.string(arg) + " -- " + File.bash_path(path)).check + bash("chown " + Bash.string(arg) + " " + File.bash_path(path)).check /* directories */