| changeset 2734 | e9bbef1b2fbe |
| parent 2733 | 1d1013313201 |
| child 3007 | e5efa177ee0c |
| 2733:1d1013313201 | 2734:e9bbef1b2fbe |
|---|---|
1 #!/bin/bash -norc |
1 #!/bin/bash -norc |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # DESCRIPTION: get value from Isabelle settings |
5 # DESCRIPTION: get values from Isabelle settings environment |
6 |
6 |
7 |
7 |
8 ## diagnostics |
8 ## diagnostics |
9 |
9 |
10 PRG=$(basename $0) |
10 PRG=$(basename $0) |