diff options
author | Daniil Baturin <daniil@baturin.org> | 2015-02-02 09:03:43 +0600 |
---|---|---|
committer | Daniil Baturin <daniil@baturin.org> | 2015-02-02 09:03:43 +0600 |
commit | 0a3e8391bed31a7e0049643a2956953201c2f3fa (patch) | |
tree | e8a5d4ff8e420688645d03290bbee179ec6e1296 /configure | |
parent | b7e7dea14bdc96cfa16f84555c609ae317a56493 (diff) | |
download | vyconf-0a3e8391bed31a7e0049643a2956953201c2f3fa.tar.gz vyconf-0a3e8391bed31a7e0049643a2956953201c2f3fa.zip |
Add basic oasis build setup.
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/configure b/configure new file mode 100755 index 0000000..6acfaeb --- /dev/null +++ b/configure @@ -0,0 +1,27 @@ +#!/bin/sh + +# OASIS_START +# DO NOT EDIT (digest: dc86c2ad450f91ca10c931b6045d0499) +set -e + +FST=true +for i in "$@"; do + if $FST; then + set -- + FST=false + fi + + case $i in + --*=*) + ARG=${i%%=*} + VAL=${i##*=} + set -- "$@" "$ARG" "$VAL" + ;; + *) + set -- "$@" "$i" + ;; + esac +done + +ocaml setup.ml -configure "$@" +# OASIS_STOP |