From: Holger V. <hol...@un...> - 2020-07-31 12:01:27
|
> I needed to create $HOME/tmp, but I assume that is intended. > I've been stumbling over this as well. Probably it is just history. Would there be a better place? Maybe simply the current working directory? Holger |