tree daa15d5156c801e0f73636942860468e3f7572fa
parent 7ec0878b74812c994e6ed313d3c06fcb616f811b
author Nicolas Lacasse <nlacasse@google.com> 1457734018 -0800
committer Nicolas Lacasse <nlacasse@google.com> 1457979873 +0000

Default JIRI_ROOT is $HOME/v23_root.

The installation instructions tell the user to set JIRI_ROOT to
$HOME/v23_root.  The contributor instructions should be consistent with
that.

Change-Id: I1cfc136693016a28c3c2711c074292726d867428