diff options
author | Kartik Agaram <vc@akkartik.com> | 2020-01-01 17:04:37 -0800 |
---|---|---|
committer | Kartik Agaram <vc@akkartik.com> | 2020-01-01 17:04:37 -0800 |
commit | 2a4088119cf41175457414dfa59bd4064b8f0562 (patch) | |
tree | 64fe184e399f9870ebd481a90eec34d51e5dff68 /archive/1.vm/copy_mu | |
parent | 23fd294d85959c6b476bcdc35ed6ad508cc99b8f (diff) | |
download | mu-2a4088119cf41175457414dfa59bd4064b8f0562.tar.gz |
5852
Diffstat (limited to 'archive/1.vm/copy_mu')
-rwxr-xr-x | archive/1.vm/copy_mu | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/archive/1.vm/copy_mu b/archive/1.vm/copy_mu new file mode 100755 index 00000000..cd4da455 --- /dev/null +++ b/archive/1.vm/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 |