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

Previous Next

Full log

View this message in rfc822 format

From: emma <bigbookofbug <at> proton.me>
To: 78289 <at> debbugs.gnu.org
Subject: [bug#78289] [PATCH] gnu: emacs-lean4-mode: add data dir to output
Date: Wed, 07 May 2025 02:25:07 +0000

[Message part 1 (text/plain, inline)]

---

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.

[Message part 2 (text/html, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.