fix(script/patch): apply changes

2019-08-09 08:52:12 -07:00 · 2019-08-09 08:52:12 -07:00 · 245d476845
commit 245d476845
parent 48f72b9b34
1 changed files with 2 additions and 0 deletions
--- a/script/patch.sh
+++ b/script/patch.sh
@ -53,5 +53,7 @@ for leanFile in `find . -name '*.lean'`; do
    diff $leanFile $leanFile.new > /dev/null
    if [ $? -ne 0 ]; then
        echo "modified $leanFile"
+        mv $leanFile.new $leanFile
+        rm -f $leanFile.old
    fi
 done