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: get values from Isabelle settings environment |
7 # DESCRIPTION: get values from Isabelle settings environment |
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] [VARNAMES ...]" |
17 echo "Usage: $PRG [OPTIONS] [VARNAMES ...]" |
49 shift $(($OPTIND - 1)) |
51 shift $(($OPTIND - 1)) |
50 |
52 |
51 |
53 |
52 # args |
54 # args |
53 |
55 |
54 [ -n "$ALL" -a $# -ne 0 ] && usage |
56 [ -n "$ALL" -a "$#" -ne 0 ] && usage |
55 |
57 |
56 |
58 |
57 ## main |
59 ## main |
58 |
60 |
59 if [ -n "$ALL" ]; then |
61 if [ -n "$ALL" ]; then |
60 env | sort |
62 env | sort |
61 else |
63 else |
62 for VAR in $* |
64 for VAR in "$@" |
63 do |
65 do |
64 if [ -n "$BASE" ]; then |
66 if [ -n "$BASE" ]; then |
65 eval "echo \$$VAR" |
67 eval "echo \$$VAR" |
66 else |
68 else |
67 eval "echo $VAR=\$$VAR" |
69 eval "echo $VAR=\$$VAR" |