diff -r 992c1b212004 -r 3e135449f797 platforms/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/platforms/Makefile	Wed Apr 08 21:58:06 2015 +0200
@@ -0,0 +1,10 @@
+dockerfiles_in = ${wildcard */Dockerfile.in}
+dockerfiles = ${dockerfiles_in:.in=}
+
+.PHONY:	all clean
+
+all:	${dockerfiles}
+clean:	; -rm -f ${dockerfiles}
+
+%:	%.in
+	../scripts/din2d $< >$@