[nongnu] elpa/proof-general f99cdf2 11/13: Misc cosmetic tweaks that occurred during GPLv3+ license work

[ELPA Syncer]

branch: elpa/proof-general
commit f99cdf289e4fa13b1dbe22de5fa08027c43f8a5a
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>

    Misc cosmetic tweaks that occurred during GPLv3+ license work
---
 doc/PG-adapting.texi    |  2 +-
 generic/proof-config.el |  5 ++++-
 lib/local-vars-list.el  | 10 +++++-----
 proof-general.el        |  4 ++--
 4 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 83874c2..6536e46 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1601,7 +1601,7 @@ input, then newlines can be retained in the input.
 
 @c TEXI DOCSTRING MAGIC: proof-shell-insert-hook
 @defvar proof-shell-insert-hook 
-Hooks run by @samp{@code{proof-shell-insert}} before inserting a command.@*
+Hook run by @samp{@code{proof-shell-insert}} before inserting a command.@*
 Can be used to configure the proof assistant to the interface in
 various ways -- for example, to observe or alter the commands sent to
 the prover, or to sneak in extra commands to configure the prover.
diff --git a/generic/proof-config.el b/generic/proof-config.el
index d3f2f19..89af386 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1626,7 +1626,7 @@ bound to `queueitems'."
   :group 'proof-shell)
 
 (defcustom proof-shell-insert-hook nil
-  "Hooks run by `proof-shell-insert' before inserting a command.
+  "Hook run by `proof-shell-insert' before inserting a command.
 Can be used to configure the proof assistant to the interface in
 various ways -- for example, to observe or alter the commands sent to
 the prover, or to sneak in extra commands to configure the prover.
@@ -1665,6 +1665,9 @@ Plastic used it to remove literate-style markup from 
`string'.
 
 See also `proof-script-preprocess' which can munge text when
 it is added to the queue of commands."
+  ;; FIXME: The docstring suggests this is used by the backend code (e.g. LEGO
+  ;; support) rather than by the end user, so maybe it shouldn't be
+  ;; a `defcustom'?
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 4d737d7..611c6b3 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -150,10 +150,10 @@ of the buffer first."
 
 
 
-;;; Local Variables: ***
-;;; fill-column: 85 ***
-;;; indent-tabs-mode: nil ***
-;;; End: ***
+;; Local Variables: ***
+;; fill-column: 85 ***
+;; indent-tabs-mode: nil ***
+;; End: ***
 
 (provide 'local-vars-list)
 ;;; local-vars-list.el ends here
diff --git a/proof-general.el b/proof-general.el
index 961fa08..af53cbc 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -69,8 +69,8 @@
   (require 'proof-site (expand-file-name "generic/proof-site" 
pg-init--pg-root)))
 
 (eval-when-compile
-  ;; FIXME: This is used during installation of the ELPA package:
-  ;; we presume that this file will be compiled before any of the files in
+  ;; FIXME: [ This is used during installation of the ELPA package ]
+  ;; We presume that this file will be compiled before any of the files in
   ;; sub-directories and we presume that all files are compiled within the same
   ;; session, so we here add to load-path all the subdirectories so
   ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find