tuned;
authorwenzelm
Thu Dec 14 14:27:37 2017 +0100 (17 months ago)
changeset 67200d49727160f0a
parent 67199 93600ca0c8d9
child 67201 4cffa4791ef7
tuned;
src/Pure/System/bash.scala
src/Pure/System/bash_syntax.ML
     1.1 --- a/src/Pure/System/bash.scala	Thu Dec 14 11:38:20 2017 +0100
     1.2 +++ b/src/Pure/System/bash.scala	Thu Dec 14 14:27:37 2017 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4        case '\f' => "$'\\f'"
     1.5        case '\r' => "$'\\r'"
     1.6        case _ =>
     1.7 -        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+-./:_".contains(ch))
     1.8 +        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
     1.9            Symbol.ascii(ch)
    1.10          else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
    1.11          else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
     2.1 --- a/src/Pure/System/bash_syntax.ML	Thu Dec 14 11:38:20 2017 +0100
     2.2 +++ b/src/Pure/System/bash_syntax.ML	Thu Dec 14 14:27:37 2017 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4            | "\r" => "$'\\r'"
     2.5            | _ =>
     2.6                if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
     2.7 -                exists_string (fn c => c = ch) "+-./:_" then ch
     2.8 +                exists_string (fn c => c = ch) "+,-./:_" then ch
     2.9                else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
    2.10                else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
    2.11                else "\\" ^ ch)