Update jenkins

samoht · Jan 30, 2013 · 83a6b20 · 83a6b20
1 parent f811688
commit 83a6b20
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/jenkins/20-opam-init.sh b/jenkins/20-opam-init.sh
@@ -5,3 +5,4 @@ cd src_ext && make distclean
 ./configure --prefix=$HOME/opam-bin/$PREFIX
 make
 make install
+make tests