From ed74755a2e8bb2f385fc1fa4d12fb2373517a3c0 Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Tue, 20 Aug 2019 22:26:46 +0200 Subject: [PATCH] add upstream issue link --- Agda-stdlib.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/Agda-stdlib.spec b/Agda-stdlib.spec index 8f782af..6bf2aec 100644 --- a/Agda-stdlib.spec +++ b/Agda-stdlib.spec @@ -41,6 +41,7 @@ dist/build/GenerateEverything/GenerateEverything # AGDA_DIR is just to ignore ~/.agda/ defaults # In 2.6.1 --no-libraries should work for this instead +# https://github.com/agda/agda/issues/4000 export AGDA_DIR=$PWD agda -i. -isrc Everything.agda