diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-11 19:09:21 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-12 00:34:19 +0000 |
| commit | b7e88b1bf82b936f8fe07c0c2c5f8621c2018f3a (patch) | |
| tree | bfec9c7f8746ea1f0682fbf0fc56654b41672c9e /reproduce/src/make/delete-me.mk | |
| parent | 595626499d20c6e3b297e72c90b5bd3f4d528e8a (diff) | |
Dependencies built at the start of the pipeline
To enable easy/proper reproduction of results, all the high-level
dependencies are now built within the pipeline and installed in a fixed
directory that is added to the PATH of the Makefile. This includes GNU Bash
and GNU Make, which are then used to run the pipeline.
The `./configure' script will first build Bash and Make within itself, then
it will build
All the dependencies are also built to be static. So after they are built,
changing of the system's low-level libraries (like C library) won't change
the tarballs.
Currently the C library and C compiler aren't built within the pipeline,
but we'll hopefully add them to the build process also.
With this change, we now have full control of the shell and Make that will
be used in the pipeline, so we can safely remove some of the generalities
we had before.
Diffstat (limited to 'reproduce/src/make/delete-me.mk')
| -rw-r--r-- | reproduce/src/make/delete-me.mk | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/reproduce/src/make/delete-me.mk b/reproduce/src/make/delete-me.mk index de72873..67f0440 100644 --- a/reproduce/src/make/delete-me.mk +++ b/reproduce/src/make/delete-me.mk @@ -63,10 +63,10 @@ $(mtexdir)/delete-me.tex: $(dm) # Here, we are first using AWK to find the minimum and maximum # values, then using it again to read each separately to use in the # macro definition. - mm=$$(awk 'BEGIN{min=99999; max=-min} \ - {if($$2>max) max=$$2; if($$2<min) min=$$2;} \ - END{print min, max}' $(dm)); \ - v=$$(echo "$$mm" | awk '{printf "%.3f", $$1}'); \ - echo "\newcommand{\deletememin}{$$v}" >> $@; \ - v=$$(echo "$$mm" | awk '{printf "%.3f", $$2}'); \ + mm=$$(awk 'BEGIN{min=99999; max=-min} + {if($$2>max) max=$$2; if($$2<min) min=$$2;} + END{print min, max}' $(dm)); + v=$$(echo "$$mm" | awk '{printf "%.3f", $$1}'); + echo "\newcommand{\deletememin}{$$v}" >> $@; + v=$$(echo "$$mm" | awk '{printf "%.3f", $$2}'); echo "\newcommand{\deletememax}{$$v}" >> $@ |