From 93b993825bbb2de1117eba9bea4fd2abe1fd0921 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 15 Feb 2020 14:36:39 -0600 Subject: [PATCH] chore(make): also remove trailing spaces in `make reindent` --- Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 0e835d01..e2392a9a 100644 --- a/Makefile +++ b/Makefile @@ -53,7 +53,9 @@ doc: reinstall: | uninstall install -reindent: ocp-indent +reindent: + @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 \ + | xargs -0 sed -i 's/[[:space:]]+$$//g' @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i