commit 08ba37a819db494371a54b7222ab2320b1c1198b
author Nicolas Lacasse <nlacasse@google.com> Fri Mar 11 14:06:58 2016 -0800
committer Nicolas Lacasse <nlacasse@google.com> Mon Mar 14 18:24:33 2016 +0000
tree daa15d5156c801e0f73636942860468e3f7572fa
parent 7ec0878b74812c994e6ed313d3c06fcb616f811b

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

content/community/contributing.md

diff --git a/content/community/contributing.md b/content/community/contributing.md
index 1244060..8c273bc 100644
--- a/content/community/contributing.md
+++ b/content/community/contributing.md
@@ -19,7 +19,7 @@
 and have added `$JIRI_ROOT/devtools/bin` to your `PATH`:
 
     # Edit to taste.
-    export JIRI_ROOT=${HOME}/vanadium
+    export JIRI_ROOT=${HOME}/v23_root
     export PATH=$PATH:$JIRI_ROOT/devtools/bin
 
 Recommended: Add the lines above to your `~/.bashrc` or similar.