Skip to content
Snippets Groups Projects
Commit 4d0e7294 authored by Patrick Steinhardt's avatar Patrick Steinhardt
Browse files

Makefile: Rename `WITH_GNU_BUILD_ID` variable

The `WITH_GNU_BUILD_ID` variable is used to determine whether GNU build
IDs should be generated or not. It's weird to disable GNU build IDs
though given that it's defined by default. Disabling would thus require
the user to pass `make WITH_GNU_BUILD_ID=`, which is not all that
intuitive.

Rename the variable to `WITHOUT_BUILD_ID` and leave it set to the empty
value. Like this, users pass `make WITHOUT_BUILD_ID=YesPlease` to
disable generation of build IDs and thus speed up their local build. Add
documentation to make this variable discoverable via `make help`.
parent 00bd206a
No related merge requests found
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment