diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2006-08-23 09:23:06 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2006-08-23 09:23:06 +0000 |
commit | 51fd985ce5de6eebdba4bb57e59e749e5360dac9 (patch) | |
tree | 9c60cb7a76dc56722168cd6c8d39c981ae2a1931 | |
parent | 2420f7174949c94384c8c436eb2aade7c4baa568 (diff) |
Comments and docstring fixes in lib and generic.
-rw-r--r-- | generic/proof-config.el | 28 | ||||
-rw-r--r-- | lib/local-vars-list.el | 5 |
2 files changed, 20 insertions, 13 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 1d77cb60..45748ee1 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1512,25 +1512,35 @@ See pg-user.el: pg-create-in-span-context-menu for more hints." (defcustom proof-prog-name nil "System command to run the proof assistant in the proof shell. May contain arguments separated by spaces, but see also `proof-prog-args'. -Suggestion: this can be set in proof-pre-shell-start-hook from -a variable which is in the proof assistant's customization -group. This allows different proof assistants to coexist -\(albeit in separate Emacs sessions)." +Suggestion: this can be set in proof-pre-shell-start-hook from a variable +which is in the proof assistant's customization group. This allows +different proof assistants to coexist \(albeit in separate Emacs sessions). + +Remark: if `proof-prog-args' is non-nil, then proof-prog-name is considered +strictly: it must contain *only* the program name with no option, spaces +are interpreted literally as part of the program name." :type 'string :group 'proof-shell) (defpgcustom prog-args nil "Arguments to be passed to `proof-prog-name' to run the proof assistant. -If non-nil, will be treated as a list of arguments for `proof-prog-name'. -Otherwise `proof-prog-name' will be split on spaces to form arguments." +If non-nil, will be treated as a list of arguments for`proof-prog-name'. +Otherwise `proof-prog-name' will be split on spaces to form arguments. + +Remark: Arguments are interpreted strictly: each one must contain only one +word, with no space (unless it is the same word). For example if the +arguments are -x foo -y bar, then the list should be '(\"-x\" \"foo\" +\"-y\" \"bar\"), notice that '(\"-x foo\" \"-y bar\") is *wrong*" + :type '(list string) :group 'proof-shell) (defpgcustom prog-env nil "Modifications to `process-environment' made before running `proof-prog-name'. -Each element should be a string of the form ENVVARNAME=VALUE. -They will be added to the environment before launching the prover (but -not pervasively)" +Each element should be a string of the form ENVVARNAME=VALUE. They will be +added to the environment before launching the prover (but not pervasively). +For example for coq on Windows you might need something like: +(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))" :type '(list string) :group 'proof-shell) diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index a79a870f..4ab62884 100644 --- a/lib/local-vars-list.el +++ b/lib/local-vars-list.el @@ -13,12 +13,9 @@ ;; ;; See the GNU General Public License version 2 for more details ;; (enclosed in the file GPL). -;; -;; See documentation in variable holes-short-doc. -;; ;;; Commentary: -;; See documentation in variable holes-doc. +;; See documentation in variable local-var-list-doc ;;; History: ;; |