aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-12-12 10:05:00 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-12-14 21:18:16 +0100
commit93a0d1ca16fd30e89e312932008106bc5503386f (patch)
tree38167b0bd4211654eb783a3771f4c7381b09ba95 /doc
parent43e54c598bbe778e67fe926e770b5235c6745045 (diff)
fix generic interrupt procedure to interrupt parallel background compilation
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi13
1 files changed, 11 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 31594b9d..be29a660 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4515,6 +4515,12 @@ the number of parallel background jobs and set
error.
@end itemize
+To abort parallel background compilation, use @code{C-c C-c}
+(@code{proof-interrupt-process}), the tool bar interrupt icon,
+the menu entry @code{Abort Background Compilation} (menu
+@code{Coq -> Auto Compilation}) or kill the Coq toplevel via
+@code{C-c C-x} (@code{proof-shell-exit}). To abort synchronous
+single threaded compilation, simply hit @code{C-g}.
@menu
@@ -4599,8 +4605,11 @@ runs up to @code{coq-max-background-compilation-jobs} coqdep and
coqc jobs in parallel in asynchronous subprocesses (or uses all
your CPU cores if @code{coq-max-background-compilation-jobs}
equals @code{'all-cpus}). Your Emacs will stay responsive during
-compilation. Use @code{C-c C-c} or the tool bar icons for
-interrupt or restart to interrupt compilation.
+compilation. To abort the background compilation process, use
+@code{C-c C-c} (@code{proof-interrupt-process}), the tool bar
+interrupt icon, the menu entry @code{Abort Background
+Compilation} (menu @code{Coq -> Auto Compilation}) or kill the
+Coq toplevel via @code{C-c C-x} (@code{proof-shell-exit}).
For the usual case, you have at most
`coq-max-background-compilation-jobs' parallel processes