Admin/user-aliases
author wenzelm
Tue, 15 Sep 2009 23:57:07 +0200
changeset 32576 20b261654e33
parent 30491 772e95280456
child 32766 87491cac8b83
permissions -rw-r--r--
double linking for improved performance of "prev"; misc tuning;
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