From 2175e39f5a45cb7bbccc790779fac1f76c05b28c Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 28 Sep 2017 13:32:17 +0200 Subject: [PATCH] fix build-dep on macOS --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index cff640c1..83a26f56 100644 --- a/Makefile +++ b/Makefile @@ -19,10 +19,10 @@ Makefile.coq: _CoqProject Makefile awk.Makefile mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp # Install build-dependencies -build-dep/opam: opam +build-dep/opam: opam Makefile # Create the build-dep package. @mkdir -p build-dep - @sed <opam 's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/' > build-dep/opam + @sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check build-dep: build-dep/opam phony -- GitLab