3931

copy_mu

@@ -0,0 +1,11 @@
+#!/usr/bin/env zsh
+# Copy binaries across mu directories for different students on a single
+# server, so we only need to build them once.
+
+cp -r $1/enumerate/enumerate $2/enumerate
+cp -r $1/cleave/cleave $2/cleave
+rm -rf $2/.build
+cp -r $1/.build $2
+cp -r $1/mu_bin $2
+cd $2
+./mu  # couple of things still get recompiled, but should now be quick