Index: tools/dev/install_files.pl
===================================================================
--- tools/dev/install_files.pl	(revision 10939)
+++ tools/dev/install_files.pl	(working copy)
@@ -182,6 +182,7 @@
            $dest .= $exe;
         }
     } elsif ($meta{include}) {
+        $dest =~ s|^include/||;
         $dest = File::Spec->catdir($options{includedir}, $dest);
     } else {
         $dest = File::Spec->catdir($options{prefix}, $dest);