diff options
| author | Bjoern B. Brandenburg <bbb@cs.unc.edu> | 2010-11-01 15:58:20 -0400 |
|---|---|---|
| committer | Bjoern B. Brandenburg <bbb@cs.unc.edu> | 2010-11-01 15:58:20 -0400 |
| commit | 0863fa86da554b29f7ff0b24b8c0ec09ed024792 (patch) | |
| tree | 7be8d0cf27d75672164888cec8ba4ce4ec7a0a15 /install_kernel.jupiter-cs | |
| parent | bd30adeeee4931e1897a6156472777fc0d5b3259 (diff) | |
make-shared-reop: allow default server to be overriden by environment
Just set SERVER in the environment prior to calling make-shared-repo
to push to a different server (or with a different user).
Diffstat (limited to 'install_kernel.jupiter-cs')
0 files changed, 0 insertions, 0 deletions