Documentation said:
15.2. Environment Variables
All the configuration files and directories used by GPS are either relative to $HOME/.gnatstudio (%HOME%.gnatstudio on Windows) if GNATSTUDIO_HOME is not set, or to $GNATSTUDIO_HOME/.gnatstudio (respectively, %GNATSTUDIO_HOME%.gnatstudio) if set.
That is, you can change the location of .gnatstudio folder but you cannot change the .gnatstudio folder name itself. Thus you cannot have several configurations in the same folder, in $HOME for instance.
It may be useful for exemple if you run different GNATStudio versions at the same time.
I propose to add the possibility to override the .gnatstudio name by a new environment variable.
Documentation said:
15.2. Environment Variables
All the configuration files and directories used by GPS are either relative to $HOME/.gnatstudio (%HOME%.gnatstudio on Windows) if GNATSTUDIO_HOME is not set, or to $GNATSTUDIO_HOME/.gnatstudio (respectively, %GNATSTUDIO_HOME%.gnatstudio) if set.
That is, you can change the location of .gnatstudio folder but you cannot change the .gnatstudio folder name itself. Thus you cannot have several configurations in the same folder, in $HOME for instance.
It may be useful for exemple if you run different GNATStudio versions at the same time.
I propose to add the possibility to override the .gnatstudio name by a new environment variable.