# HG changeset patch
# User wenzelm
# Date 933156428 -7200
# Node ID 37178f53ed4d8aab6262ce6ca7eefe44432c877f
# Parent  f1e787b90fdc0a2604709fb60a185db5bbfd35e4
mkdir contrib;

diff -r f1e787b90fdc -r 37178f53ed4d Admin/makedist
--- a/Admin/makedist	Wed Jul 28 10:28:34 1999 +0200
+++ b/Admin/makedist	Wed Jul 28 12:07:08 1999 +0200
@@ -132,7 +132,7 @@
 cp Admin/index.html $DISTBASE
 rm -rf Admin Doc
 
-mkdir src
+mkdir src contrib
 mv $LOGICS src
 
 mv Distribution/* .