Date: Tue, 16 Mar 2021 09:31:24 -0400 From: Chet Ramey <chet.ra...@case.edu> Message-ID: <31aff163-9e61-d34a-be79-40c7e09a8...@case.edu>
| If you want to set PWD instead of letting cd/pushd/popd manage it, | all bets are off. I agree with that as far as what you get when you expand $PWD (even the pwd command, so using `pwd` as an alternative if PWD has been manually set is not necessarily going to work), and even the way the cd command works, but the bash man page says: \w the current working directory, with $HOME abbreviated with a tilde (uses the value of the PROMPT_DIRTRIM variable) Nothing about $PWD there, it should be the current working directory, according to that definition, and one thing that changing PWD does not do is change the current working directory. Of course, the simple fix to this is to change the man page, so refer to $PWD instead of "the current working directory". | Just like setting HOME changes tilde expansion. It does, but that's not really an analogy, ~/ is defined to be ${HOME}/ so if changing HOME did not have that effect then ~ expansion would be broken. If changing HOME had any effect on ~kre/ (given that the relevant user name is used, such that it should produce what is normally in an unaltered $HOME) however, then that would be a problem. kre