Disable precompiled headers in 'nix develop'

They're still enabled in regular builds though.
This commit is contained in:
Eelco Dolstra 2020-09-21 13:28:51 +02:00
parent fd721f06f5
commit d110fdd03f
2 changed files with 2 additions and 5 deletions

View file

@ -136,7 +136,7 @@
enableParallelBuilding = true; enableParallelBuilding = true;
makeFlags = "profiledir=$(out)/etc/profile.d"; makeFlags = "profiledir=$(out)/etc/profile.d PRECOMPILE_HEADERS=1";
doCheck = true; doCheck = true;
@ -334,9 +334,6 @@
# syntax-check generated dot files, it still requires some # syntax-check generated dot files, it still requires some
# fonts. So provide those. # fonts. So provide those.
FONTCONFIG_FILE = texFunctions.fontsConf; FONTCONFIG_FILE = texFunctions.fontsConf;
# To test building without precompiled headers.
makeFlagsArray = [ "PRECOMPILE_HEADERS=0" ];
}; };
# System tests. # System tests.

View file

@ -1,4 +1,4 @@
PRECOMPILE_HEADERS ?= 1 PRECOMPILE_HEADERS ?= 0
print-var-help += \ print-var-help += \
echo " PRECOMPILE_HEADERS ($(PRECOMPILE_HEADERS)): Whether to use precompiled headers to speed up the build"; echo " PRECOMPILE_HEADERS ($(PRECOMPILE_HEADERS)): Whether to use precompiled headers to speed up the build";