diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..2ce4b1fb6089ca9432076aeaa34378e2f2b47f47 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,6 @@ +/examples/in_progress/ export-ignore +/misc/ export-ignore +/ROADMAP export-ignore +/DEVELOPER.readme export-ignore +/opam/ export-ignore +.gitignore export-ignore diff --git a/Makefile.in b/Makefile.in index 4d95c8e96f108e34100b5e9803f05e77eba90205..eb84b605241cd64b99ff8f1fe17494b5714b4ae3 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1743,23 +1743,15 @@ wc: ######### NAME = why3-@VERSION@ -DISTRIB_DIR = distrib/$(NAME) -DISTRIB_TAR = $(DISTRIB_DIR).tar.gz - -# TODO? -# share/zsh ? -# symbolic links in share/ ? +# see .gitattributes for the list of files that are not distributed EXTRA_DIST = configure doc/manual.pdf -NODIST = examples/in_progress/ misc/ ROADMAP DEVELOPER.readme opam/ dist: $(EXTRA_DIST) - rm -rf $(DISTRIB_TAR) $(DISTRIB_DIR) - mkdir -p $(DISTRIB_DIR) - for d in `git ls-tree -d -r --name-only HEAD`; do mkdir $(DISTRIB_DIR)/$$d; done - for f in `git ls-tree -r --name-only HEAD` $(EXTRA_DIST); do cp $$f $(DISTRIB_DIR)/$$f; done - rm `find $(DISTRIB_DIR) -name .gitignore` - cd $(DISTRIB_DIR); rm -rf $(NODIST) + rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz + mkdir -p distrib/ + git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/ + for f in $(EXTRA_DIST); do cp $$f distrib/$(NAME)/$$f; done cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar