aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorPaul Steckler2018-02-23 14:23:19 -0500
committerGaƫtan Gilbert2018-05-16 13:28:10 +0200
commita2f4a43833a29a5ede5905225b814c33e3a46132 (patch)
treebb2bd38286a6d51451df109e476862ab75ca65de /Makefile
parent3f480c993311d19b152deb6bb4dc561188d76fc7 (diff)
add unit tests to test suite
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 793afb661e..f914de5a61 100644
--- a/Makefile
+++ b/Makefile
@@ -58,7 +58,7 @@ FIND_SKIP_DIRS:='(' \
-name '_build_ci' -o \
-name '_install_ci' -o \
-name 'user-contrib' -o \
- -name 'coq-makefile' -o \
+ -name 'test-suite' -o \
-name '.opamcache' -o \
-name '.coq-native' \
')' -prune -o