| changeset 15903 | c93ae0eb9631 |
| parent 15902 | 0fce3f919aec |
| child 15937 | b74dfcdeac1b |
| 15902:0fce3f919aec | 15903:c93ae0eb9631 |
|---|---|
9 # |
9 # |
10 |
10 |
11 . ~/.bashrc |
11 . ~/.bashrc |
12 |
12 |
13 ## settings |
13 ## settings |
14 MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de # berghofe@in.tum.de lp15@cam.ac.uk" |
14 MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de haftmann@in.tum.de # berghofe@in.tum.de lp15@cam.ac.uk" |
15 |
15 |
16 DOCDIR=$HOME/Doc |
16 DOCDIR=$HOME/Doc |
17 DISTPREFIX=~/tmp/isadist |
17 DISTPREFIX=~/tmp/isadist |
18 |
18 |
19 MAXTIME=1800 |
19 MAXTIME=1800 |