[Re: [GRASS-dev] BASH question about quitting GIS Manager]