diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-11-24 18:40:01 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-11-24 18:40:01 +0000 |
commit | 042563213e3a2641dd914470cfd98d63aef67b64 (patch) | |
tree | 1970791bc017ddf3ebdb5945c05e49b904b06ec5 /reproduce/software/bash/git-post-checkout | |
parent | cae8be3505acee2f58dea4ff60978aee2f8787ed (diff) |
Project's Makefiles run with no builtin rules or variables
Until now, after removing all environment variables, we were just giving
Make the top Makefile to execute. By default, for every target, Make will
try many built-in rules (which is good when compiling programs, but
redundant in other cases). All these checkings also populate the debugging
output of Make (with `-d'). So its easier and slightly faster to just tell
Make to ignore builtin rules and variables.
With this commit, to address this issue, the `project' script runs
`.local/bin/make' with `--no-builtin-rules' and `--no-builtin-variables'.
Diffstat (limited to 'reproduce/software/bash/git-post-checkout')
0 files changed, 0 insertions, 0 deletions