From 61f04320b01df3efd72f73adc9a3bafe311f3523 Mon Sep 17 00:00:00 2001 From: Healfdene Goguen Date: Wed, 6 May 1998 15:28:55 +0000 Subject: Simpler procedure for compiling emacs lisp. Added coq-info-dir so that script-management.info can be hard-coded. --- INSTALL | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 27d5ad75..8771d108 100644 --- a/INSTALL +++ b/INSTALL @@ -1,20 +1,14 @@ To install, put the .el files in an appropriate directory and compile them using `byte-compile-file' in xemacs: - M-x byte-compile-file proof-dependencies-xemacs.el - M-x byte-compile-file proof-fontlock.el - M-x byte-compile-file proof.el - M-x byte-compile-file lego-fontlock.el - M-x byte-compile-file coq-fontlock.el - M-x byte-compile-file lego.el - M-x byte-compile-file coq.el - M-x byte-compile-file pbp.el + M-0 M-x byte-recompile-directory If you want to use this mode for Coq, you need to make sure you have an appropriate version, which is from later than 1 March 1998. -Put the compiled emacs files and the file -script-management.info in a suitable directory for local emacs files, -as suggested by your system administrator. +Put the compiled emacs files and the file script-management.info in a +suitable directory for local emacs files, as suggested by your system +administrator. Otherwise, alter the coq-info-dir in coq.el to a +hard-coded path where you put the file script-management.info. Install coqtags or legotags in a standard place. -- cgit v1.2.3