diff options
| author | Pierre-Marie Pédrot | 2019-05-11 18:52:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-11 18:52:43 +0200 |
| commit | ff58928a9ccd8d7cdf6a23a30cc569abae3e1cf7 (patch) | |
| tree | 85990f41640268a595ff618952ffc334178fee15 /doc | |
| parent | 1fb2819d57d16196fd8dc7cb49e72b9e1d22758e (diff) | |
| parent | d911384de18874b98c20bf25e444f1d356af4249 (diff) | |
Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS + adding a go-to-end binding + improving documentation
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 6cbd00f45d..efb5df720a 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a |