3931

1 files changed, 11 insertions, 0 deletions

diff --git a/copy_mu b/copy_mu
new file mode 100755
index 00000000..cd4da455
--- /dev/null
+++ b/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