diff options
Diffstat (limited to 'generic/pg-pamacs.el')
| -rw-r--r-- | generic/pg-pamacs.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index bb765c2c..4958b360 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -228,7 +228,9 @@ which can be changed by sending commands. In this case, NAME stands for the internal setting, flag, etc, for the proof assistant, and a :setting and :type value should be provided. The :type of NAME should be one of 'integer, 'float, -'boolean, 'string. +'boolean, 'string. Other types are not supported (see +`proof-menu-entry-for-setting'). They will yield an error when +constructing the proof assistant menu. The function `proof-assistant-format' is used to format VAL. |