chore: remove external header target

there is no need to update the header file, and we already patched it in
925745f0e3 so new version won't work
unless patched
This commit is contained in:
youben11
2022-04-06 09:31:24 +01:00
committed by Ayoub Benaissa
parent cae23bc15d
commit 91ccea9b6b

View File

@@ -5,8 +5,6 @@ PARALLEL_EXECUTION_ENABLED=OFF
CC_COMPILER=
CXX_COMPILER=
EXTERNAL_HEADERS=include/boost-single-header/outcome.hpp
KEYSETCACHEDEV=/tmp/KeySetCache
KEYSETCACHECI=../KeySetCache
@@ -63,9 +61,6 @@ $(BUILD_DIR)/configured.stamp:
-DPython3_EXECUTABLE=${Python3_EXECUTABLE}
touch $@
include/boost-single-header/outcome.hpp:
wget https://github.com/ned14/outcome/raw/master/single-header/outcome.hpp -O $@
build-initialized: $(EXTERNAL_HEADERS) $(BUILD_DIR)/configured.stamp
doc: build-initialized