Commit a2723dc2 authored by Clément Fumex's avatar Clément Fumex
Browse files

change readme to not have to modify proof-general sources

parent 06756a5e
To use Proof General with Why3ITP make a symbolic link of this folder
into the proof general folder (typically ~/.emacs.d/lisp/PG/) and add
the line
To use Proof General with Why3ITP add the following lines in your
.emacs after the line loading proof-general itself.
(whyitp "whyitp" "whyitp")
to the definition of "proof-assistant-table-default" int
(autoload 'whyitp-mode "(MY_PATH_TO_WHY3)/share/whyitp/whyitp.el" "Major mode for Why3 ITP." t)
(setq auto-mode-alist (cons '("\\.whyitp" . whyitp-mode) auto-mode-alist))
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment