Default theme is not default

--===============0766594014039944641==
Content-Type: multipart/alternative; boundary=f403045e1f24513446054f1f002d

--f403045e1f24513446054f1f002d
Content-Type: text/plain; charset=UTF-8

Hello, I was working in GPS 2016 (20160515) and decided to change the
editor's theme.
I looked at some of them, didn't like them and decided to switch back to
default theme...
and found out that the default theme is not the previous theme which was by
default.
So, is it possible to make the default theme be default? Or at least to
have a possibility
to switch back to the previous theme?



-- 
Regards, Denis Obrezkov

--f403045e1f24513446054f1f002d
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hello, I was working in GPS 2016 (20160515) and decided to=
 change the editor&#39;s theme.<div>I looked at some of them, didn&#39;t li=
ke them and decided to switch back to default theme...</div><div>and found =
out that the default theme is not the previous theme which was by default.<=
/div><div>So, is it possible to make the default theme be default? Or at le=
ast to have a possibility</div><div>to switch back to the previous theme?</=
div><div><br></div><div><br clear=3D"all"><div><br></div>-- <br><div class=
=3D"gmail_signature">Regards, Denis Obrezkov</div>
</div></div>

--f403045e1f24513446054f1f002d--

--===============0766594014039944641==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
gps-users mailing list
[email protected]
http://lists.adacore.com/mailman/listinfo/gps-users

--===============0766594014039944641==--