diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-01 16:29:02 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-01 16:29:02 +0000 |
| commit | a8e0880b296b876f7bbd2e5ba37a54dcc2eb09d5 (patch) | |
| tree | 1aa023b7a91f419c75c2ffbe75118f58aa17f98e /lego/lego.el | |
| parent | 684a1fb1c829213fdfbd5db482c54d380828e544 (diff) | |
Replaced string COMMENT by constant proof-no-command.
Diffstat (limited to 'lego/lego.el')
| -rw-r--r-- | lego/lego.el | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/lego/lego.el b/lego/lego.el index 90927a37..540a887b 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -85,6 +85,14 @@ :type 'string :group 'lego-settings) +;; FIXME da: this doesn't belong here, it's only used by lego. +;; (and it shouldn't be called w3-* !!) +(defun w3-remove-file-name (address) + "Remove the file name in a World Wide Web address" + (string-match "://[^/]+/" address) + (concat (substring address 0 (match-end 0)) + (file-name-directory (substring address (match-end 0))))) + (defcustom lego-www-latest-release (concat (w3-remove-file-name lego-www-home-page) "html/release-1.3/") @@ -269,8 +277,7 @@ proof-terminal-string)))) (setq span (next-span span 'type))) - (or ans - "COMMENT"))) + (or ans proof-no-command))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Other stuff which is required to customise script management ;; |