diff --git a/vendor/update-cmdliner.sh b/vendor/update-cmdliner.sh new file mode 100755 index 00000000..dd1079d1 --- /dev/null +++ b/vendor/update-cmdliner.sh @@ -0,0 +1,21 @@ +#!/bin/bash + +version=1.0.0 + +set -e -o pipefail + +TMP="$(mktemp -d)" +trap "rm -rf $TMP" EXIT + +rm -rf cmdliner +mkdir -p cmdliner/src + +(cd $TMP && opam source cmdliner.$version) + +SRC=$TMP/cmdliner.$version + +cp -v $SRC/LICENSE.md cmdliner +cp -v $SRC/src/*.{ml,mli} cmdliner/src + +git checkout cmdliner/src/{jbuild,result.ml} +git add -A .