diff options
| author | Daniil Baturin <daniil@baturin.org> | 2024-11-07 18:02:08 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-11-07 18:02:08 +0000 |
| commit | 196fdd7fdf6dcf751b7364c59e34278bfd0193e3 (patch) | |
| tree | cfeff0991481c8281e24cf1698b20a76854059a4 /configure | |
| parent | dd9271b4304c6b1a5a2576821d1b2b8fd3aa6bf5 (diff) | |
| parent | 9b90d3cc4da72c13ef4270150e4b547ff03fc813 (diff) | |
| download | vyconf-196fdd7fdf6dcf751b7364c59e34278bfd0193e3.tar.gz vyconf-196fdd7fdf6dcf751b7364c59e34278bfd0193e3.zip | |
Merge pull request #11 from jestabro/vyconf-minimal
T6718: use the vyconf daemon for validation of set commands
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/configure b/configure deleted file mode 100755 index 6acfaeb..0000000 --- a/configure +++ /dev/null @@ -1,27 +0,0 @@ -#!/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 |