summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-05-14 15:36:52 -0700
committerGitHub <noreply@github.com>2018-05-14 15:36:52 -0700
commit0c6681152ca422f7ace1bd1d3c3dac7823de2c14 (patch)
tree84b7ab5df824cb26df70b437b6bb7ad41c30aadb /contrib
parentb5264346e85bc7ca0235048f686cc252c60b0014 (diff)
Add contrib/get-symfpu for downloading symfpu. (#1905)
Diffstat (limited to 'contrib')
-rw-r--r--contrib/Makefile.am6
-rwxr-xr-xcontrib/get-symfpu24
2 files changed, 30 insertions, 0 deletions
diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 72e354d97..4d61e88f4 100644
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -10,8 +10,14 @@ EXTRA_DIST = \
new-theory \
configure-in-place \
depgraph \
+ get-abc \
get-antlr-3.4 \
+ get-cadical \
get-cryptominisat \
+ get-glpk-cut-log \
+ get-lfsc-checker \
+ get-script-header.sh \
+ get-symfpu \
get-win-dependencies \
mac-build \
run-script-smtcomp2014 \
diff --git a/contrib/get-symfpu b/contrib/get-symfpu
new file mode 100755
index 000000000..f48d2d5b4
--- /dev/null
+++ b/contrib/get-symfpu
@@ -0,0 +1,24 @@
+#!/bin/bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+
+wdir="symfpu-CVC4"
+
+if [ -e $wdir ]; then
+ echo "error: file or directory "$wdir" exists; please move it out of the way." >&2
+ exit 1
+fi
+
+commit="bdc0ad4cc49b5d590b4d8492199249e392c3368d"
+
+mkdir $wdir
+cd $wdir
+git clone https://github.com/martin-cs/symfpu.git symfpu
+cd symfpu
+git checkout $commit
+
+echo
+echo "Using symfpu commit $commit"
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-symfpu
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback