IntenseWebs/pgadmin4
3
0
Fork 0
mirror of https://github.com/pgadmin-org/pgadmin4.git synced 2025-02-25 18:55:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Add infrastructure for managing configurable keyboard shortcuts.

Browse Source
This commit is contained in:
Harshal Dhumal
2018-01-25 12:49:06 +00:00
committed by Dave Page
parent 7c985695b7
commit 66341e6947
7 changed files with 885 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
web/pgadmin/preferences/static/css/preferences.css
View File

@@ -25,10 +25,6 @@ div.pgadmin-preference-body div.ajs-content {
bottom: 0px !important;
}
.preferences_content .control-label, .preferences_content .pgadmin-controls {
min-width: 100px !important;
}
.pgadmin-preference-body {
min-width: 300px !important;
min-height: 400px !important;
@@ -40,3 +36,15 @@ div.pgadmin-preference-body div.ajs-content {
min-height: 480px !important;
}
}
.keyboard-shortcut-label {
font-weight: normal !important;
}
.preferences_content input[type="checkbox"]:focus {
outline: 5px auto -webkit-focus-ring-color;
}
.preferences_content .pgadmin-controls input[type="checkbox"] {
margin-left: -20px !important;
}