diff options
Diffstat (limited to 'src/tools/PGINDENT')
| -rw-r--r-- | src/tools/PGINDENT | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/tools/PGINDENT b/src/tools/PGINDENT new file mode 100644 index 0000000000..2b0b72799a --- /dev/null +++ b/src/tools/PGINDENT @@ -0,0 +1,24 @@ +#!/bin/sh +trap "rm -f /tmp/$$" 0 1 2 3 15 +entab </dev/null >/dev/null +if [ "$?" -ne 0 ] +then echo "Go to the src/tools/entab directory and do a 'make' and 'make install'." >&2 + echo "This will put the 'entab' command in your path." >&2 + echo "Then run $0 again." + exit 1 +fi +indent -st </dev/null >/dev/null +if [ "$?" -ne 0 ] +then echo "You do not appear to have 'indent' installed on your system." >&2 + exit 1 +fi +for FILE +do + cat $FILE | + sed 's;/\* *---;/*---;g' | + indent -bad -bap -bbb -bc -bl -d0 -ncdb -nce -cli1 -di16 -nfc1 \ + -lp -nip -nbc -psl -di1 -i4 -st | + detab -t8 | + entab -qc -t4 | + sed 's;/\*---;/* ---;g' >/tmp/$$ && cat /tmp/$$ >$FILE +done |