mirror of
https://github.com/servo/servo
synced 2026-04-25 17:15:48 +02:00
232d434701
Similar to about:config from firefox. All preferences are editable; editing them mid-runtime is not guaranteed to cause any effects. This is separate from servo:preferences, which selectively groups and exposes preferences. This probably would become more useful if/when preferences become persistent. <img width="1136" height="880" alt="Screenshot 2025-10-31 at 10 19 57 PM" src="https://github.com/user-attachments/assets/2ef759d8-06a4-457f-b9df-331cc3525338" /> Followup work: - Remove `getStringPreference`, `getIntPreference`, and `getBoolPreference`. Using `getPreference` and `preferenceType` is more flexible. - Make more of these config options work on the fly. - Allow for reverting config options. --------- Signed-off-by: Ashwin Naren <arihant2math@gmail.com>
57 lines
672 B
CSS
57 lines
672 B
CSS
body {
|
|
padding: 0;
|
|
display: flex;
|
|
flex-direction: column;
|
|
}
|
|
|
|
input {
|
|
border-radius: 4px;
|
|
}
|
|
|
|
.search {
|
|
height: 24px;
|
|
width: calc(100% - 6px);
|
|
margin-top: 12px;
|
|
margin-bottom: 12px;
|
|
margin-right: 6px;
|
|
padding: 4px;
|
|
}
|
|
|
|
table {
|
|
border-collapse: collapse;
|
|
}
|
|
|
|
table, th, td {
|
|
border: 0;
|
|
}
|
|
|
|
tr:nth-child(2n) {
|
|
background-color: #f0f0f0;
|
|
}
|
|
|
|
.value-editor {
|
|
margin: 2px;
|
|
padding: 2px;
|
|
}
|
|
|
|
.switch-button {
|
|
margin: 2px;
|
|
padding: 2px;
|
|
border-radius: 4px;
|
|
background: #cfcfcf;
|
|
border: 0;
|
|
}
|
|
|
|
.icon {
|
|
width: 24px;
|
|
height: 24px;
|
|
}
|
|
|
|
.hidden {
|
|
display: none;
|
|
}
|
|
|
|
.default {
|
|
font-weight: bold;
|
|
}
|