From 91ccea9b6b77c424745b85f4d08dea5d1bbe90ed Mon Sep 17 00:00:00 2001
From: youben11 <ayoub.benaissa@zama.ai>
Date: Wed, 6 Apr 2022 09:31:24 +0100
Subject: [PATCH] chore: remove external header target

there is no need to update the header file, and we already patched it in
925745f0e3256d39bc65cd2d1ab3abc000b4e372 so new version won't work
unless patched
---
 compiler/Makefile | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/compiler/Makefile b/compiler/Makefile
index 256fc1a95..5a9ec728a 100644
--- a/compiler/Makefile
+++ b/compiler/Makefile
@@ -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