From 314a5e371234e48c7fa0a5ef0b41f5110834d91d Mon Sep 17 00:00:00 2001
From: Michael Wallner <mike@php.net>
Date: Wed, 30 Sep 2015 15:07:55 +0200
Subject: [PATCH] duh

---
 .gitignore    |  1 +
 Makefile.frag | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 Makefile.frag

diff --git a/.gitignore b/.gitignore
index 48963a5..ce11f5a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,3 +26,4 @@ run-tests.php
 .libs/
 /php_raphf_api.h
 Doxyfile.bak
+!/Makefile.frag
diff --git a/Makefile.frag b/Makefile.frag
new file mode 100644
index 0000000..94dc490
--- /dev/null
+++ b/Makefile.frag
@@ -0,0 +1,16 @@
+# provide headers in builddir, so they do not end up in /usr/include/ext/raphf/src
+
+PHP_RAPHF_HEADERS := $(addprefix $(PHP_RAPHF_BUILDDIR)/,$(PHP_RAPHF_HEADERS))
+
+$(PHP_RAPHF_BUILDDIR)/%.h: $(PHP_RAPHF_SRCDIR)/src/%.h
+	@cat >$@ <$<
+
+all: raphf-build-headers
+clean: raphf-clean-headers
+
+.PHONY: raphf-build-headers
+raphf-build-headers: $(PHP_RAPHF_HEADERS)
+
+.PHONY: raphf-clean-headers
+raphf-clean-headers:
+	-rm -f $(PHP_RAPHF_HEADERS)
-- 
2.30.2