diff options
| -rwxr-xr-x | home/.local/bin/whinclude | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/home/.local/bin/whinclude b/home/.local/bin/whinclude new file mode 100755 index 00000000..26445cdc --- /dev/null +++ b/home/.local/bin/whinclude @@ -0,0 +1,11 @@ +#!/bin/sh +set -eu + +echo "#include <${1}>" | +cc ${CFLAGS:-} -E -x c - | +sed -En ' + /^# [0-9]+ "[^<]/{ + s/.*"([^"]+)".*/\1/p + q + } +' |