diff options
| author | Pierre-Yves Strub | 2016-01-05 22:17:24 -0800 |
|---|---|---|
| committer | Pierre-Yves Strub | 2016-01-05 22:19:48 -0800 |
| commit | ab782048a148271919ed2e11debff674892f4c95 (patch) | |
| tree | 138c376fd4e8af75082d4ab29fd75b07769450cc /etc/utils | |
| parent | 7780c22d12484785f480057df9f3396a52fb19f5 (diff) | |
do not use `sed -i' in ssrcoqdep -- this is not portable
This prevents compilation of ssreflect on OS-X/*BSD.
Diffstat (limited to 'etc/utils')
| -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 ;; *) ;; |