From cb1a56bbda0d873fe3e9dd7ea8a3906c2ed9cbfd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Thu, 21 Sep 2017 22:09:04 +0200
Subject: [PATCH] Indicate how to load ProofGeneral in .emacs.

---
 README.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/README.md b/README.md
index 29b3f06..39a2abf 100644
--- a/README.md
+++ b/README.md
@@ -185,6 +185,13 @@ sudo rm -rf $TARGET
 sudo mv /tmp/PG $TARGET
 ```
 
+Enable ProofGeneral by adding the following line to your `.emacs` file:
+```elisp
+(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
+```
+If desired, ProofGeneral can be further
+[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
+
 ## Bibliography
 
 [Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),