diff options
| author | Owen W. Taylor <otaylor@fishsoup.net> | 2012-10-05 13:35:58 -0400 |
|---|---|---|
| committer | Owen W. Taylor <otaylor@fishsoup.net> | 2012-10-05 13:35:58 -0400 |
| commit | aa1a84e67765f0f1ee514c2335d9e6678ad2c6e1 (patch) | |
| tree | ba37ab3749d4cb673c4ea8d71c168e7032e5d2e0 /tools | |
| parent | 9395f310d64cb2cb441f9ef0d5702cda476294f6 (diff) | |
| download | gnome-shell-aa1a84e67765f0f1ee514c2335d9e6678ad2c6e1.tar.gz | |
gnome-shell-build-setup.sh: add a note about removing install directory
If the user relocates from ~/gnome-shell to ~/gnome, they need to
remove the install directory or left-over paths will cause problems.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/build/gnome-shell-build-setup.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tools/build/gnome-shell-build-setup.sh b/tools/build/gnome-shell-build-setup.sh index d546bb4ac..fd511aa1f 100755 --- a/tools/build/gnome-shell-build-setup.sh +++ b/tools/build/gnome-shell-build-setup.sh @@ -304,11 +304,13 @@ WARNING: The old source and install directory '$HOME/gnome-shell' exists, but '$HOME/gnome' doesn't. An empty $HOME/gnome will be created. - To avoid starting again from scratch you should remove the empty directory - and move your old '$HOME/gnome-shell' to '$HOME/gnome': + To avoid starting again from scratch you should remove the empty directory, + move your old '$HOME/gnome-shell' to '$HOME/gnome', and delete the old + install directory: rm -rf $HOME/gnome mv $HOME/gnome-shell $HOME/gnome + rm -rf $HOME/gnome/install EOF fi |