| changeset 15937 | b74dfcdeac1b |
| parent 15903 | c93ae0eb9631 |
| child 16615 | e665dafdd2b8 |
| 15936:817ac93ee786 | 15937:b74dfcdeac1b |
|---|---|
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 haftmann@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 makarius@sketis.net" |
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 |