aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--utils/inst1
1 files changed, 1 insertions, 0 deletions
diff --git a/utils/inst b/utils/inst
index 9c15496..c3c26e2 100644
--- a/utils/inst
+++ b/utils/inst
@@ -55,6 +55,7 @@ checkdiff() {
G="${g#$1}"
COMMIT=$( cd "$1/$G" && git rev-parse HEAD )
echo "Checkout of git repository: $2/$G"
+ # TODO this doesn't seems to work
( cd "$2/$G" && git --work-tree=. checkout -f "$COMMIT" )
done
else