From 4e0c2376bfc02461b35101264b51f0fb158d2451 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 27 Oct 1998 18:04:30 +0000
Subject: Comments

---
 Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 80a13b0b..8670de12 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,9 @@
 ## Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ##
 ##
-##  make compile
+##  make compile	- make .elc's in a single session
+##  make all		- make .elc's in separate sessions
+##
 ##
 ## $Id$
 ## 
-- 
cgit v1.2.3