diff options
| -rwxr-xr-x | etc/utils/ssrcoqdep | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/utils/ssrcoqdep b/etc/utils/ssrcoqdep index 8ef5422..20e1281 100755 --- a/etc/utils/ssrcoqdep +++ b/etc/utils/ssrcoqdep @@ -13,7 +13,7 @@ case $key in *.v) mkdir -p $(dirname bkpcoqdep/$key) cp $key bkpcoqdep/$key - sed "s/^From.*//" -i $key + sed "s/^From.*//" bkpcoqdep/$key > $key ;; *) ;; |