Make distr

diff --git a/Makefile b/Makefile
index f6524101046caabb18450882d9cdb87a73d937c7..989c2a1af1e553307b1f9b4c1c0c946409dd4dc5 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,10 @@
 all:
        @echo "Nothing to be done for 'all'"
 
+.PHONY: distr
+distr:
+       ./mk-distr
+
 .PHONY: html
 html:
        $(MAKE) -C docs html