patacongo commented on pull request #2463:
URL: https://github.com/apache/incubator-nuttx/pull/2463#issuecomment-738859711
After running indent.sh, I do the following:
# Run the indent tool on the file. This requires manual fixups
# including removing the bogus blank line at the top of the
# file and and putting the final */ of multi-line comments on a
# separate line
tools/indent.sh $file
# After indent.sh, fix header files with bad pre-processor indentation
filename=$(basename $(file))
extension="${filename##*.}"
if ("X$extension" == "Xh"); then
sed -i -e "s/# /#/g" $file
fi
Do you think this should be added to tools/indent.sh?
----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
us...@infra.apache.org
