diff options
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/utils/ssrcoqdep | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/etc/utils/ssrcoqdep b/etc/utils/ssrcoqdep index dd1c068..8ef5422 100755 --- a/etc/utils/ssrcoqdep +++ b/etc/utils/ssrcoqdep @@ -11,6 +11,7 @@ key="$1" case $key in *.v) + mkdir -p $(dirname bkpcoqdep/$key) cp $key bkpcoqdep/$key sed "s/^From.*//" -i $key ;; @@ -23,5 +24,9 @@ done COQBIN="$(dirname $(which coqtop))/" $COQBIN/coqdep $args -mv bkpcoqdep/* . -rmdir bkpcoqdep +for f in $(find bkpcoqdep -name "*.v") +do +mv $f ${f##bkpcoqdep/} +done + +rm -rf bkpcoqdep |