From 237c361b0f4417c94e9e6edda695d2518a9a0391 Mon Sep 17 00:00:00 2001 From: Anton Felix Lorenzen Date: Sun, 15 Apr 2018 16:59:32 +0200 Subject: [PATCH] Check all files in travis.ci script --- .gitignore | 1 + .travis.yml | 5 +---- index.sh | 5 +++++ 3 files changed, 7 insertions(+), 4 deletions(-) create mode 100755 index.sh diff --git a/.gitignore b/.gitignore index 171a389..cee2c70 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ *.agdai +index.agda \ No newline at end of file diff --git a/.travis.yml b/.travis.yml index 4df3276..9919c9d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -8,8 +8,5 @@ services: before_install: - docker pull scottfleischman/agda:2.5.2 -env: -- AGDA_FILE="src/API/Theorems.agda" - script: -- docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; agda '$AGDA_FILE +- docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; ./index.sh; agda -i . -i src/ index.agda' diff --git a/index.sh b/index.sh new file mode 100755 index 0000000..361686a --- /dev/null +++ b/index.sh @@ -0,0 +1,5 @@ +rm -rf index.agda; +echo "module index where" >> index.agda; +for i in $( find src -name "*.agda" | sed 's/src\/\(.*\)\.agda/\1/' | sed 's/\//\./g' | sort ); do + echo "import $i" >> index.agda; +done