[ #3159 ] Added more missing --no-default-libraries options.

(cherry picked from commit 20a73f2)
agda · Jul 18, 2018 · bfd18ad · bfd18ad
1 parent c33d4a7
commit bfd18ad
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/test/LaTeXAndHTML/Tests.hs b/test/LaTeXAndHTML/Tests.hs
@@ -139,6 +139,7 @@ mkLaTeXOrHTMLTest k agdaBin inp =
                    [ "-i" ++ testDir
                    , inp
                    , "--ignore-interfaces"
+                   , "--no-libraries"
                    ] ++ extraFlags
     res@(ret, _, _) <- PT.readProcessWithExitCode agdaBin agdaArgs T.empty
     if ret /= ExitSuccess then

diff --git a/test/api/Makefile b/test/api/Makefile
@@ -2,7 +2,7 @@ TOP = ../..
 
 include $(TOP)/mk/paths.mk
 
-AGDA = $(AGDA_BIN) -v0
+AGDA = $(AGDA_BIN) -v0 --no-libraries
 
 all : Issue1168.api PrettyInterface.api ScopeFromInterface.api