2017-12-06 22:51:49 +04:00
|
|
|
#! /bin/sh
|
|
|
|
|
|
|
|
|
|
set -e
|
|
|
|
|
|
|
|
|
|
script_dir="$(cd "$(dirname "$0")" && echo "$(pwd -P)/")"
|
|
|
|
|
src_dir="$(dirname "$script_dir")"
|
|
|
|
|
|
|
|
|
|
. "$script_dir"/opam-remove.sh
|
|
|
|
|
|
2018-07-05 01:08:20 +04:00
|
|
|
echo
|
|
|
|
|
echo "## Unpinning tezos packages..."
|
|
|
|
|
|
|
|
|
|
opam pin remove $packages > /dev/null 2>&1
|
