From 8fba6db8f135212bf220da53964f3362a605663c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 1 Oct 2010 11:49:23 +0000 Subject: proof-script-command-separator: removed (always a space) --- CHANGES | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGES b/CHANGES index fd151eb7..341d38a5 100644 --- a/CHANGES +++ b/CHANGES @@ -134,6 +134,7 @@ proof-shell-abort-goal-regexp: removed (ordinary response) proof-shell-error-or-interrupt-seen: removed, use p-s-last-output-kind proof-script-next-entity-regexps,next-entity-fn: removed (func-menu dead) + proof-script-command-separator: removed (always a space) *** Simplified version of comint now used for proof shell (internal) To improve efficiency, a cut-down version of comint is now used. -- cgit v1.2.3