From 8de08ca9bac7c175ebbf1aa588634a63bfc77a4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Fri, 21 Oct 2022 16:38:22 +0200 Subject: [PATCH] [distrib] make-distrib.sh uses the same tar options as 'make distrib' before dune. --- dev/make-distrib.sh | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh index b57c2da9cb4..391182f63a0 100755 --- a/dev/make-distrib.sh +++ b/dev/make-distrib.sh @@ -174,7 +174,11 @@ fi echo $VERSION_SAFE > $TMP_DIR/$FRAMAC/VERSION echo $VERSION_CODENAME > $TMP_DIR/$FRAMAC/VERSION_CODENAME -tar czf $FRAMAC_TAR.gz -C $TMP_DIR $FRAMAC +DATE="$(date +%F)" + +tar czf $FRAMAC_TAR.gz -C $TMP_DIR $FRAMAC \ + --numeric-owner --owner=0 --group=0 --sort=name --mode='a+rw' \ + --mtime="$DATE Z" if [[ "$CI_LINK" == "yes" ]]; then ln $FRAMAC_TAR.gz "frama-c.tar.gz" -- GitLab