Subject: [bug#78289] [PATCH] gnu: emacs-lean4-mode: add data dir to output

From: emma <[email-masked]>
Date: Wed, 07 May 2025 02:25:07 +0000

---

gnu/packages/emacs-xyz.scm | 11 +++++++++++
1 file changed, 11 insertions(+)

diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
index 50a6f4c386..fd919aa210 100644
--- a/gnu/packages/emacs-xyz.scm
+++ b/gnu/packages/emacs-xyz.scm
@@ -3081,6 +3081,17 @@ (define-public emacs-lean4-mode
;; TODO: Just emacs-magit-section instead of emacs-magit would be enough.
(propagated-inputs
(list emacs-compat emacs-lsp-mode emacs-dash emacs-magit))
+ (arguments
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'install-data
+ (lambda _
+ (let ((data (string-append #$output
+ "/share/emacs/site-lisp/"
+ "lean4-mode-1.1.2/data")))
+ (mkdir-p data)
+ (copy-recursively "data" data)))))))
(synopsis "Lean 4 major mode for Emacs")
(description "This package provides a major mode for the Lean theorem
prover, version 4.")

base-commit: d110f7dd006f4e47aa56de3cdaf5bb4b82eb5ca2
--
2.49.0

emma (bigbookofbug)
EF515F7D600717781DF9AB2E0FB1CF2867A117F5

Sent with [Proton Mail](https://proton.me/mail/home) secure email.