diff options
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel index e73a60da..9a688241 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -82,8 +82,9 @@ DEVELOPERS=\ -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" - +-u "assia Assia Mahboubi assia.mahboubi@inria.fr" \ +-u "monnier Stefan Monnier monnier@iro.umontreal.ca" \ +-u "tews Hendrik Tews tews@os.inf.tu-dresden.de" # PRERELEASE_PREFIX is used to match PRERELEASE_TAG in sed # line in tag target below, which edits $(DOWNLOADHTML) |