patch ssrcoqdep

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