| 
     
      
      
      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  |