# HG changeset patch
# User wenzelm
# Date 1484578254 -3600
# Node ID 14c760e0e1cffe012833d3e8978874abd5c8d81d
# Parent  ba72a13eb78c507995797ce135fefb504bcb0242
tuned -- nicer generated bash source;

diff -r ba72a13eb78c -r 14c760e0e1cf src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun Jan 15 16:47:42 2017 +0100
+++ b/src/Pure/System/bash.scala	Mon Jan 16 15:50:54 2017 +0100
@@ -24,7 +24,7 @@
       case '\f' => "$'\\f'"
       case '\r' => "$'\\r'"
       case _ =>
-        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
+        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+-./:_".contains(ch))
           Symbol.ascii(ch)
         else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
         else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
diff -r ba72a13eb78c -r 14c760e0e1cf src/Pure/System/bash_syntax.ML
--- a/src/Pure/System/bash_syntax.ML	Sun Jan 15 16:47:42 2017 +0100
+++ b/src/Pure/System/bash_syntax.ML	Mon Jan 16 15:50:54 2017 +0100
@@ -24,7 +24,7 @@
           | "\r" => "$'\\r'"
           | _ =>
               if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
-                exists_string (fn c => c = ch) "-./:_" then ch
+                exists_string (fn c => c = ch) "+-./:_" then ch
               else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
               else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
               else "\\" ^ ch)