aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-21 16:23:26 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-21 16:23:26 +0000
commit506c3dc502fcdb3c19412307af673d4173724482 (patch)
treedcff8bb32ba92975703bd3ef0989bc1aec488765 /generic
parent22300c60dbc8834bea4d44d4c83b748238aea5a9 (diff)
docstring
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 50f9a557..bf12bc9b 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -461,7 +461,9 @@ process.
It is up to the proof assistant how much context is cleared: for
example, theories already loaded may be \"cached\" in some way,
-so that loading them the next time round does not require re-processing."
+so that loading them the next time round only performs a re-linking
+operation, not full re-processing. (One way of caching is via
+object files, used by Lego and Coq)."
(interactive)
(if proof-shell-busy
(progn