diff --git a/doc/install.html b/doc/install.html index f17dce5bdd4c82..79ae9664c89af6 100644 --- a/doc/install.html +++ b/doc/install.html @@ -106,6 +106,12 @@
+Note: changes made to a profile
file may not apply until the
+next time you log into your computer. Alternatively, you can apply them to the
+current shell with a command like source $HOME/.profile
.
+