diff options
Diffstat (limited to 'generic/pg-pbrpm.el')
-rw-r--r-- | generic/pg-pbrpm.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 9f331476..21f0c02f 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -4,9 +4,11 @@ ;; Authors: Jean-Roch SOTTY, Christophe Raffalli ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; - ;; analysis of the goal buffer +(require 'proof-utils) ;; for proof-face-specs + + (defvar pg-pbrpm-use-buffer-menu t "if t, pbrpm will use a menu displayed in a dialog fram instead of a popup menu") |