@set localpintostarpath /usr/class/cs140/pintos/pintos.tar.gz
@set localpintoshttppath http://@/www.stanford.edu/@/class/@/cs140/@/pintos/@/pintos.@/tar.gz
@set localpintosbindir /usr/class/cs140/`uname -m`/bin
@set localpintostarpath /usr/class/cs140/pintos/pintos.tar.gz
@set localpintoshttppath http://@/www.stanford.edu/@/class/@/cs140/@/pintos/@/pintos.@/tar.gz
@set localpintosbindir /usr/class/cs140/`uname -m`/bin