-add support for -R and -I -as in coq-load-path

-improve documentation (and reorder stuff)

1 files changed, 5 insertions, 1 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index fe516973..0f8a1047 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3409,7 +3409,7 @@ restarting the process.
 Function run when a proof-shell buffer is killed.@*
 Try to shut down the proof process nicely and clear locked
 regions and state variables.  Value for @samp{@code{kill-buffer-hook}} in
-shell buffer, alled by @samp{@code{proof-shell-bail-out}} if process exits.
+shell buffer, called by @samp{@code{proof-shell-bail-out}} if process exits.
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-shell-exit
@@ -3424,6 +3424,10 @@ without confirmation.
 
 The kill function uses @samp{<PA>-quit-timeout} as a timeout to wait
 after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process.
+
+This function should not be called if
+@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of
+@samp{@code{proof-shell-kill-function}} will give strange errors.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-shell-bail-out