mirror of
https://github.com/aclist/dztui.git
synced 2026-11-03 16:42:13 +01:00
chore: move is_developer to UserPrefs
This commit is contained in:
1 parent
2184622918
commit
5a76c37839
5 files changed
+11
-13
No files matched your search
@@ -167,7 +167,10 @@ class Options(Gtk.Box):
|
||||
|
||||
developers=Gtk.Button(label="Developers", halign=Gtk.Align.START)
|
||||
developers.connect("clicked", self._on_developers_clicked)
|
||||
if self.controller.get_developer_mode():
|
||||
|
||||
prefs = self.controller.get_prefs()
|
||||
is_developer = prefs.is_developer
|
||||
if is_developer:
|
||||
grid.attach(
|
||||
developers, 1, 0, self.DEFAULT_WIDTH, self.DEFAULT_HEIGHT
|
||||
)
|
||||
|
||||
Reference in new issue
Block a user