diff --git a/script/patch.sh b/script/patch.sh
index f0d6fc8b2f..81a78acd2a 100755
--- 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