diff options
| -rw-r--r-- | Makefile.devel | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index 76ccbd3b..613801b4 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -74,7 +74,7 @@ DEVELOPERS=\ -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" \ +-u "markus Markarius makarius@sketis.net" \ -u "pier Pierre Courtieu courtieu@lri.fr" \ -u "crr Christophe Raffalli Christophe.Raffalli@univ-savoie.fr" \ -u "pxc Paul Callaghan P.C.Callaghan@durham.ac.uk" \ |