diff options
| -rw-r--r-- | doc/PG-adapting.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index bf375235..a6e35719 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3739,7 +3739,7 @@ Proof General. ;; ;; Copyright (C) 1999 LFCS Edinburgh. ;; -;; Author: David Aspinall <David.Aspinall@ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@@ed.ac.uk> ;; ;; $Id$ ;; |