Admin/user-aliases
author immler@in.tum.de
Mon, 16 Mar 2009 14:26:30 +0100
changeset 30542 eb720644facd
parent 30491 772e95280456
child 32766 87491cac8b83
permissions -rw-r--r--
have remote script interrupted like the other provers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29561
d8c2712749b8 lcp = paulson
haftmann
parents: 29555
diff changeset
     1
lcp paulson
29554
7e5e5ebb7bf7 added churn script
haftmann
parents:
diff changeset
     2
norbert.schirmer@web.de schirmer
29555
8938f89973f3 corrected user aliases
haftmann
parents: 29554
diff changeset
     3
urbanc@in.tum.de urbanc
30491
772e95280456 more user aliases;
wenzelm
parents: 29561
diff changeset
     4
nipkow@lapbroy100.local nipkow
772e95280456 more user aliases;
wenzelm
parents: 29561
diff changeset
     5
chaieb@chaieb-laptop chaieb
772e95280456 more user aliases;
wenzelm
parents: 29561
diff changeset
     6
immler@in.tum.de immler