diff --git a/format.sh b/format.sh deleted file mode 100755 index 2da2b67d5..000000000 --- a/format.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/bash - -echo "# Removing tabs" -find ./ -regex "^\.\(/[a-zA-Z0-9_-.]*\)*.ml[il]?" -exec sed -i 's/ //g' {} \; -echo "# Indent files" -find ./ -regex "^\.\(/[a-zA-Z0-9_-.]*\)*.ml[il]?" -exec ocp-indent -i {} \;