aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2003-02-18 17:24:54 +0000
committerDavid Aspinall2003-02-18 17:24:54 +0000
commitb1a4e47933153b640c8bca1c959257041f451882 (patch)
treefc23a9e9aa96fde9f6cfb10c44d892335f28b04a
parent90a2ffa45ff32db8afc7875c0b489c58993a2653 (diff)
Comments.
-rw-r--r--generic/pg-metadata.el3
-rw-r--r--generic/pg-xhtml.el2
2 files changed, 5 insertions, 0 deletions
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index f8c3c67b..d8563199 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -12,6 +12,9 @@
;; - add file dependency information to proof scripts individually
;; (can approximate from the transitive closure that is included files list)
;;
+;; NB: THIS FILE NOT YET USED: once required by PG,
+;; must be added to main dist by editing Makefile.devel
+;;
(require 'pg-xml)
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el
index c5f09ad9..402e7a85 100644
--- a/generic/pg-xhtml.el
+++ b/generic/pg-xhtml.el
@@ -6,6 +6,8 @@
;;
;; $Id$
;;
+;; NB: THIS FILE NOT YET USED: once required by PG,
+;; must be added to main dist by editing Makefile.devel
(require 'pg-xml)