diff options
Diffstat (limited to 'doc/Makefile')
-rw-r--r-- | doc/Makefile | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile index aeeadacb..e1e11be4 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -3,6 +3,8 @@ ## ## Author: David Aspinall <da@dcs.ed.ac.uk> ## +## Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +## ## $Id$ ## ########################################################################### |