aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
diff options
context:
space:
mode:
authorDavid Aspinall2009-08-20 11:23:18 +0000
committerDavid Aspinall2009-08-20 11:23:18 +0000
commita26e2e3089ab01d11c6cbca10abf6b168a2a41c7 (patch)
tree15f0d97bef1329a2e029fabdb847b0c57381f07e /generic/proof-script.el
parentc440ded61788d0718065c494f7f19065da0e7e03 (diff)
proof-one-command-per-line: change default, use in proof-insert-pbp-command.
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index ac44c9d9..8252838b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2279,7 +2279,7 @@ appropriate."
(proof-activate-scripting)
(let (span)
(proof-goto-end-of-locked)
- (insert "\n") ;; could be user opt
+ (if proof-one-command-per-line (insert "\n"))
(insert cmd)
(setq span (span-make (proof-locked-end) (point)))
(span-set-property span 'type 'pbp)