equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # DESCRIPTION: prepare logic session directory |
7 # DESCRIPTION: prepare logic session directory |
6 |
8 |
7 |
9 |
8 ## diagnostics |
10 ## diagnostics |
9 |
11 |
10 PRG=$(basename $0) |
12 PRG=$(basename "$0") |
11 |
13 |
12 function usage() |
14 function usage() |
13 { |
15 { |
14 echo |
16 echo |
15 echo "Usage: $PRG [OPTIONS] [LOGIC] NAME" |
17 echo "Usage: $PRG [OPTIONS] [LOGIC] NAME" |
67 |
69 |
68 |
70 |
69 # args |
71 # args |
70 |
72 |
71 |
73 |
72 if [ $# -eq 1 ]; then |
74 if [ "$#" -eq 1 ]; then |
73 LOGIC="$ISABELLE_LOGIC" |
75 LOGIC="$ISABELLE_LOGIC" |
74 DIR_NAME="$1"; shift |
76 DIR_NAME="$1"; shift |
75 elif [ $# -eq 2 ]; then |
77 elif [ "$#" -eq 2 ]; then |
76 LOGIC="$1"; shift |
78 LOGIC="$1"; shift |
77 DIR_NAME="$1"; shift |
79 DIR_NAME="$1"; shift |
78 else |
80 else |
79 usage |
81 usage |
80 fi |
82 fi |