diff options
Diffstat (limited to 'generic/pg-pgip.el')
| -rw-r--r-- | generic/pg-pgip.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index bc1d152b..dc00426f 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -92,6 +92,7 @@ ((eq pgip 'usespgml)) ((or (eq pgip 'haspref) + (eq pgip 'oldhaspref) ;; FIXME: see note above about oldhaspref (eq pgip 'prefval)) ;; Update preferences view/menu (proof-assistant-menu-update)) |