aboutsummaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 14:06:28 -0400
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 14:06:28 -0400
commit2f44fe53e1a598b524e11cda3dc9ce7a04534247 (patch)
tree47a77eb4ed8fea3ac5ec99c5bf5ad9131ba44fd9 /.travis.yml
parente101fc5dd8783d029d7a4933c7ccca4a67ed3874 (diff)
parent3d8afe1c9bd905e3a62523e87a2aa7e5d9f5093d (diff)
Merge with plv/master
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml11
1 files changed, 11 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 000000000..9bea40d88
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,11 @@
+language: generic
+
+sudo: required
+dist: trusty
+
+addons:
+ apt:
+ packages:
+ - coq
+
+script: make COQPATH="$(pwd)/coqprime" TIMED=1 -j2