diff options
| author | Josselin Poiret <[email protected]> | 2023-04-30 12:10:06 +0200 |
|---|---|---|
| committer | Josselin Poiret <[email protected]> | 2023-06-04 10:59:35 +0200 |
| commit | 8203e8f3c9cf0462abb9f03e42e578fe28599c36 (patch) | |
| tree | fbb74cb82a4df6f3fec7fec826da81d4426e7e65 /gnu/packages/patches/agda-categories-use-find.patch | |
| parent | c1f8bcbbda4d90dc98d5e808049f008dffe6b979 (diff) | |
gnu: Add agda-categories.
* gnu/packages/patches/agda-categories-use-find.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.
* gnu/packages/agda.scm: New variable agda-categories.
Diffstat (limited to 'gnu/packages/patches/agda-categories-use-find.patch')
| -rw-r--r-- | gnu/packages/patches/agda-categories-use-find.patch | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/gnu/packages/patches/agda-categories-use-find.patch b/gnu/packages/patches/agda-categories-use-find.patch new file mode 100644 index 0000000000..772352a0cb --- /dev/null +++ b/gnu/packages/patches/agda-categories-use-find.patch @@ -0,0 +1,31 @@ +From 53922aedd81d5111d9007b41235aa12eaa2a863d Mon Sep 17 00:00:00 2001 +Message-Id: <53922aedd81d5111d9007b41235aa12eaa2a863d.1682840933.git.dev@jpoiret.xyz> +From: Josselin Poiret <[email protected]> +Date: Sun, 30 Apr 2023 09:48:21 +0200 +Subject: [PATCH] Use find instead of git ls-tree in Makefile + +From: Josselin Poiret <[email protected]> + +--- + Makefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/Makefile b/Makefile +index 158802d1..68846579 100644 +--- a/Makefile ++++ b/Makefile +@@ -11,7 +11,7 @@ html: Everything.agda + agda ${RTSARGS} --html -i. Everything.agda + + Everything.agda: +- git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda ++ find src -iname '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda + + clean: + find . -name '*.agdai' -exec rm \{\} \; + +base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9 +prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55 +-- +2.39.2 + |