Merge pull request #13 from strub/master

do not use `sed -i' in ssrcoqdep -- this is not portable

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
     ;;
     *)
     ;;