| changeset 9237 | 161fb7f00414 |
| parent 9208 | 7bf28980c521 |
| child 9788 | df671fa2562a |
| 9236:899b83e8d2e1 | 9237:161fb7f00414 |
|---|---|
8 PRG=$(basename $0) |
8 PRG=$(basename $0) |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [GRAPHFILE]" |
13 echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -d delete file after use" |
16 echo " -d delete file after use" |
17 echo |
17 echo |
18 exit 1 |
18 exit 1 |