Add a script to upgrade vendor/cmdliner
This commit is contained in:
parent
d69a7c577a
commit
868f75f146
|
@ -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 .
|
Loading…
Reference in New Issue