diff options
Diffstat (limited to 'tools/find_includes')
| -rwxr-xr-x | tools/find_includes | 52 |
1 files changed, 0 insertions, 52 deletions
diff --git a/tools/find_includes b/tools/find_includes deleted file mode 100755 index 6dfb406fa3..0000000000 --- a/tools/find_includes +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/env bash - -phase=phase0 - -phase0() { - phase=phase0 - local line="$1" - case "$line" in - '#include'*|'typedef '*';') - phase1 "$line" - ;; - *) - ;; - esac -} - -phase1() { - phase=phase1 - local line="$1" - case "$line" in - '') - ;; - '#include'*) - ;; - 'typedef '*';') - ;; - *) - phase2 "$line" - ;; - esac -} - -phase2() { - phase=phase2 - local line="$1" - printf '%s\n' "$line" - cat -} - -main() { - current_file="$1" - set -o pipefail - { - IFS='' - while read -r line; do - "$phase" "$line" - IFS='' - done - } < "$current_file" | grep '^#include' | ifne printf '%s\n' "$current_file" -} - -main "$@" |