equal
deleted
inserted
replaced
43 |
43 |
44 (* system path representations *) |
44 (* system path representations *) |
45 |
45 |
46 val platform_path = Path.implode o Path.expand; |
46 val platform_path = Path.implode o Path.expand; |
47 |
47 |
48 fun shell_quote s = |
48 val shell_quote = enclose "'" "'"; |
49 if exists_string (fn c => c = "'") s then |
|
50 error ("Illegal single quote in path specification: " ^ quote s) |
|
51 else enclose "'" "'" s; |
|
52 |
|
53 val shell_path = shell_quote o platform_path; |
49 val shell_path = shell_quote o platform_path; |
54 |
50 |
55 |
51 |
56 (* current working directory *) |
52 (* current working directory *) |
57 |
53 |