aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel
index a3266eea..4ad041bd 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -72,7 +72,7 @@
# NB: must use TAB as separator in list below.
DEVELOPERS=\
--u "da David Aspinall da+pg-da@inf.ed.ac.uk" \
+-u "da David Aspinall da@inf.ed.ac.uk" \
-u "gkein Gerwin Klein gklein@in.tum.de" \
-u "sberghof Stefan Berghofer berghofe@in.tum.de" \
-u "markus Markus Wenzel da+pg-wenzelm@inf.ed.ac.uk" \