diff options
| author | Makarius Wenzel | 2000-11-21 18:18:57 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-11-21 18:18:57 +0000 |
| commit | d6d7a0be9aa3c56917b7d956b322953b5305506e (patch) | |
| tree | 73a94db2dc5c7946b82746c702d47e1caa191841 /hol98/example.sml | |
| parent | a51550f20684e07ecf98fe8c7a0fb78ea0953163 (diff) | |
converted from sh back to bash;
use "#!/usr/bin/env bash" as interpreter to determine bash from PATH;
handle spaces in file names;
Diffstat (limited to 'hol98/example.sml')
0 files changed, 0 insertions, 0 deletions