tree 96c7a5f05f73295adb422c03aad642b3a0704049
parent f765ba69c9eb7d2d253bfb5ee9750b13a88c6bdd
author Nicolas Lacasse <nlacasse@google.com> 1456944039 -0800
committer Nicolas Lacasse <nlacasse@google.com> 1456944039 -0800

website: bootstrap.sh should recommend adding .jiri_root/scripts to PATH

JIRI_ROOT/devtools/bin will be deperated at some point, and we are
encouraging users to use JIRI_ROOT/.jiri_root/scripts instead.

Also remove unused "run" and "must" functions.

Change-Id: I856498ac23872e863e13b5ba2ee8ee1e6f9bae73