minimize-requires.py is writing extra .bak files

[jdchristensen]

minimize-requires is making a .bak file for files it doesn't actually change (see file2.v below) and is making both a .bak and a .bak.bak file for files it does change (see file1.v below).

$ cat file1.v
Require Import file2.

Definition foo := Type.
$ cat file2.v
Definition bar := Type.
$ ls *bak
ls: cannot access '*bak': No such file or directory
$ cat _CoqProject 
file1.v
file2.v

$ /tmp/jdc/coq-tools/minimize-requires.py --all -f _CoqProject --in-place .bak
getting file1.v (/tmp/jdc/testminreq/file1.v)
getting file1.glob (/tmp/jdc/testminreq/file1.glob)
getting file2.v (/tmp/jdc/testminreq/file2.v)
getting file2.glob (/tmp/jdc/testminreq/file2.glob)
getting file1.glob (/tmp/jdc/testminreq/file1.glob)

Running command: "coqc" "-R" "." "Top" "/tmp/tmp8rotjxqk.v" "-q"

The timeout for coqc has been set to: 3
Running coq on initial contents...
Successful change
Saving final version of file1.v...
getting file2.glob (/tmp/jdc/testminreq/file2.glob)
Running coq on initial contents...
Successful change
Saving final version of file2.v...
$ ll *bak
-rw-rw---- 1 jdc jdc 24 Jun  9 10:47 file1.v.bak
-rw-rw---- 1 jdc jdc 47 Jun  9 10:43 file1.v.bak.bak
-rw-rw---- 1 jdc jdc 24 Jun  9 10:46 file2.v.bak
$ cmp file2.v file2.v.bak
$ cmp file1.v file1.v.bak
$ cmp file1.v file1.v.bak.bak
file1.v file1.v.bak.bak differ: byte 1, line 1

Note the "Successful change" for file2.v, which had no changes needed. And the extra .bak for file1.