A few clarifications in README

1 files changed, 14 insertions, 6 deletions

diff --git a/README.md b/README.md
index ca94b511..24477c8e 100644
--- a/README.md
+++ b/README.md
@@ -8,23 +8,31 @@ This is version 4.4 of Proof General.
 
 ## Setup
 
-Download and install Proof General from GitHub:
+Remove old versions of Proof General, then download and install the new release from GitHub:
 
 ```
 git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
-make -C ~/.emacs.d/lisp/PG
+cd ~/.emacs.d/lisp/PG
+make
 ```
 
-Then add the following to your .emacs:
+Then add the following to your `.emacs`:
 
 ```
 ;; Open .v files with Proof General's Coq mode
 (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")
 ```
 
+If Proof General complains about a version mismatch, make sure that the shell's `emacs` is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On Mac in particular you'll probably need something like
+
+```
+make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
+```
+
 ## More info
 
 See
+
     INSTALL	     for installation details.
     COPYING	     for license details.
     COMPATIBILITY    for version compatibility information.
@@ -38,9 +46,9 @@ Links:
     Wiki:		  http://proofgeneral.inf.ed.ac.uk/wiki
     Lists:		  http://proofgeneral.inf.ed.ac.uk/mailinglist
 
-Supported proof assistants:  Coq, Isabelle, LEGO, PhoX
-Experimental (less useful):  CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf
-        Obsolete instances:  Demoisa,Lambda-Clam,Plastic
+* Supported proof assistants:  Coq, Isabelle, LEGO, PhoX
+* Experimental (less useful):  CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf
+* Obsolete instances:  Demoisa,Lambda-Clam,Plastic
 
 A few example proofs are included in each prover subdirectory.  The
 "root2" proofs of the irrationality of the square root of 2 were