changeset 16002 | e0557c452138 |
parent 15570 | 8d8c70b41bab |
child 16261 | 28803c418b59 |
16001:554836ed1f1b | 16002:e0557c452138 |
---|---|
94 (case file_info name of |
94 (case file_info name of |
95 "" => NONE |
95 "" => NONE |
96 | s => SOME (Info s)) |
96 | s => SOME (Info s)) |
97 end; |
97 end; |
98 |
98 |
99 val exists = isSome o info; |
99 val exists = is_some o info; |
100 |
100 |
101 |
101 |
102 (* directories *) |
102 (* directories *) |
103 |
103 |
104 fun system_command cmd = |
104 fun system_command cmd = |