do no distribute generated files in tarball

parent 5736ab82
......@@ -1101,6 +1101,8 @@ $(DISTRIB_TAR): doc/manual.pdf
ln -s ../theories $(DISTRIB_DIR)/share/theories
cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
rm -f $(DISTRIB_DIR)/src/
cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
# distrib export: source export-doc export-www export-examples export-examples-c linux
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment