[ travis ] ignore other sources of unsafe code

agda · Aug 8, 2018 · 3de5757 · 3de5757
1 parent 0a62e0c
commit 3de5757
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/travis/index.sh b/travis/index.sh
@@ -6,5 +6,8 @@ for i in $( find src -name "*.agda" \
           | sort \
           ); do
   echo "import $i" >> index.agda;
-  if [[ ! $i == *Unsafe ]]; then echo "import $i" >> safe.agda; fi
+  if [[ ! $i == *Unsafe \
+     && ! $i == Reflection \
+     && ! $i == IO* \
+     && ! $i == *TrustMe ]]; then echo "import $i" >> safe.agda; fi
 done