From 2a07a14efdb79d635de8fd1c9951f6c2ee952b32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Henry?= Date: Tue, 24 Jul 2018 18:11:18 +0200 Subject: [PATCH] Makefile: no need to pin local packages --- scripts/install_build_deps.raw.sh | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/scripts/install_build_deps.raw.sh b/scripts/install_build_deps.raw.sh index bd1c038c1..dd892ea71 100755 --- a/scripts/install_build_deps.raw.sh +++ b/scripts/install_build_deps.raw.sh @@ -5,8 +5,6 @@ src_dir="$(dirname "$script_dir")" . "$script_dir"/version.sh -. "$script_dir"/opam-pin.sh +opams=$(find "$src_dir/vendors" "$src_dir/src" -name \*.opam -print) -opam depext $packages - -opam install $packages --deps-only --with-test +opam install $opams --deps-only --with-test