diff options
| -rw-r--r-- | doc/docstring-magic.el | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index b36643ce..58eee9ef 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.el @@ -1,4 +1,13 @@ -;; Ensure that non-compiled versions of everything is loaded +;; doc/docstring-magic.el -- hack for using texi-docstring-magic. +;; +;; Copyright (C) 1998 LFCS Edinburgh. +;; Author: David Aspinall +;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +;; +;; Ensure that non-compiled versions of everything are loaded. +;; +;; $Id$ +;; (setq load-path (append '("../generic/" "../isa/" "../lego/" "../coq/") load-path)) |