3931
This commit is contained in:
parent
248e789e7c
commit
9f67a02cbb
|
@ -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
|
Loading…
Reference in New Issue