From 0cf477dbfa51cc3435c97d673f4ea5d5a5d39077 Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Wed, 28 Mar 2018 12:46:48 +0200
Subject: [PATCH] small fix to installed headers

---
 src/maketools/install.headers | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/maketools/install.headers b/src/maketools/install.headers
index b123c5e99..5720f9682 100644
--- a/src/maketools/install.headers
+++ b/src/maketools/install.headers
@@ -8,15 +8,22 @@ shift
 
 script=""
 includedir=
-for dir in $*
+dirs=$*
+
+for dir in $dirs
 do
 script="$script"'
 s|^# *include *"'$dir'/|#include "../'$dir'/|'
 done
 export LC_ALL=C
 
-for file in */*.h
+for dir in $dirs
+do
+for file in $dir/*.h
 do
-  mkdir -p "$where/${file%/*}"
-  cat $file | sed "$script" > "$where/$file"
+  if test -e $file ; then
+    mkdir -p "$where/${file%/*}"
+    cat $file | sed "$script" > "$where/$file"
+  fi
+done
 done
-- 
GitLab