diff options
| -rw-r--r-- | Makefile.devel | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index 0d89c988..fa2a3ceb 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -59,7 +59,7 @@ # Arguments for rcs2log for ChangeLog target DEVELOPERS=\ --u "da David Aspinall da@dcs.ed.ac.uk" \ +-u "da David Aspinall da@proofgeneral.org" \ -u "markus Markus Wenzel wenzelm@informatik.tu-muenchen.de" \ -u "pier Pierre Courtieu courtieu@lri.fr" \ -u "crr Christophe Raffalli Christophe.Raffalli@univ-savoie.fr" \ |