You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.