diff options
| -rw-r--r-- | Makefile.devel | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.devel b/Makefile.devel index b3058d3d..86930a3f 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -83,6 +83,7 @@ DEVELOPERS=\ -u "tms Thomas Kleymann da+pg-tms@inf.ed.ac.uk" \ -u "djs Dilip Sequiera da+pg-djs@inf.ed.ac.uk" \ -u "hhg Healfdene Goguen da+pg-hhg@inf.ed.ac.uk" \ +-u "gklein Gerwin Klein gerwin.klein@nicta.com.au" \ -u "assia Assia Mahboubi assia.mahboubi@inria.fr" |