-
Ignacio Casal Quinteiro authored
We moved the gnome terminal profile settings to our settings. For now we use always our settings because gnome terminal has not been ported to gsettings yet.
33bc0189
We moved the gnome terminal profile settings to our settings. For now we use always our settings because gnome terminal has not been ported to gsettings yet.