mirror of
https://github.com/doomemacs/doomemacs
synced 2025-08-01 12:17:25 -05:00
lang/coq: fix file-missing proof-site errors
Occasionally happens after the first time running `doom refresh` (after installing proof-general).
This commit is contained in:
@ -1,4 +1,15 @@
|
|||||||
;;; lang/coq/autoload.el -*- lexical-binding: t; -*-
|
;;; lang/coq/autoload.el -*- lexical-binding: t; -*-
|
||||||
|
|
||||||
|
;; HACK `proof-general' ascertains its own library path at compile time in its
|
||||||
|
;; autoloads file using `byte-compile-current-file' (and stores it in
|
||||||
|
;; `pg-init--script-full-path'). This means that when
|
||||||
|
;; `doom-package-autoload-file' is created and byte-compiled,
|
||||||
|
;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it
|
||||||
|
;; tries to load `proof-site'. We prevent this by defining these two variables
|
||||||
|
;; early, in our own autoloads file.
|
||||||
|
;;;###autoload
|
||||||
|
(setq pg-init--script-full-path (locate-library "proof-general")
|
||||||
|
pg-init--pg-root (file-name-directory pg-init--script-full-path))
|
||||||
|
|
||||||
;;;###autoload
|
;;;###autoload
|
||||||
(add-hook 'coq-mode-hook #'company-coq-mode)
|
(add-hook 'coq-mode-hook #'company-coq-mode)
|
||||||
|
Reference in New Issue
Block a user