use the good name

This commit is contained in:
ed 2025-08-12 19:03:34 +00:00
parent d8662aeb0e
commit 69d9878acd

View file

@ -16746,7 +16746,7 @@ var settheme = (function () {
var html = [],
cb = ebi('themes'),
itheme = ax.indexOf(theme[0]) * 2 + (light ? 1 : 0),
names = ['classic dark', 'classic light', 'pm-monokai', 'flat light', 'vice', 'hotdog stand', 'hacker', 'hi-con', 'win95 dark', 'win95'];
names = ['classic dark', 'classic light', 'pm-monokai', 'flat light', 'vice', 'hotdog stand', 'hacker', 'hi-con', 'phi95 dark', 'phi95'];
for (var a = 0; a < themes; a++)
html.push('<option value="{0}">{0} ┃ {1}</option>'.format(a, names[a] || 'custom'));