You've already forked gnatstudio
mirror of
https://github.com/AdaCore/gnatstudio.git
synced 2026-02-12 12:42:33 -08:00
And add a mechanism to copy the old .gps directory to .gnatstudio the first time. Rename keys6.xml to keys.xml when importing the old .gpr directory. Change-Id: I1e1ea2c123ae772a547561737e2309d4c081f239
This directory contains a number of python scripts, that show how GPS can be extended through this scripting language. To use any of these scripts, copy the file to your $HOME/.gnatstudio/plug-ins directory.