[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.
master
Gabriel Scherer 2019-01-08 15:02:09 +01:00
parent d9ee956c9c
commit 7712a919e3
1 changed files with 2 additions and 2 deletions

View File

@ -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`\\\"")