get files from ../include/linux if not here

diff --git a/linux/kinstall.sh b/linux/kinstall.sh
index efb242087db5b54569bc8665f12408578e6c6a6f..0391a231c3fca4230cb76fe793e8e3f7491f28d4 100755 (executable)
--- a/linux/kinstall.sh
+++ b/linux/kinstall.sh
@@ -115,6 +115,14 @@ newer () {
 
 installfile () {
   BASE=`basename $1`
+  if [ ! -e $BASE ]; then
+    if [ -e ../include/linux/$BASE ]; then
+      BASE=../include/linux/$BASE
+    else
+      echo Could not find source file $BASE !
+      false ; return
+    fi
+  fi
   if newer $1 $BASE; then
     echo $1 is not older than $BASE, skipping
     return 0