From 7712a919e3481a2edc2918fc8b6f6d115b3fc16f Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 8 Jan 2019 15:02:09 +0100 Subject: [PATCH] [minor] fix dune build The script would previously use `grep 'ARCH=' Makefile.config` to locate the ARCH-setting line of the configuration. But now the configuration looks like this ### Set ARCH=none if your machine is not supported ARCH=amd64 and the 'grep' call trips up on the comment. This commit uses '^ARCH' instead. Hopefully that is portable to other system's `grep` command. --- asmcomp/dune | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/asmcomp/dune b/asmcomp/dune index aea36976f..a208b56e5 100644 --- a/asmcomp/dune +++ b/asmcomp/dune @@ -22,7 +22,7 @@ (glob_files i386/*.ml) (glob_files power/*.ml) (glob_files s390x/*.ml)) - (action (bash "cp `grep 'ARCH=' %{conf} | cut -d'=' -f2`/*.ml ."))) + (action (bash "cp `grep '^ARCH=' %{conf} | cut -d'=' -f2`/*.ml ."))) (rule (targets emit.ml) @@ -37,7 +37,7 @@ (action (progn (with-stdout-to contains-input-name - (bash "echo `grep 'ARCH=' %{conf} | cut -d'=' -f2`/emit.mlp")) + (bash "echo `grep '^ARCH=' %{conf} | cut -d'=' -f2`/emit.mlp")) (with-stdout-to %{targets} (progn (bash "echo \\# 1 \\\"`cat contains-input-name`\\\"")