mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
[ docs ] Fix strange indentation on WebKit-based browsers (partial fix for #1367)
This commit is contained in:
parent
5bbcb29a38
commit
182a3caa3e
@ -157,7 +157,6 @@ dd.fixity {
|
||||
}
|
||||
|
||||
.name {
|
||||
display: table-cell;
|
||||
white-space: nowrap;
|
||||
width: 0;
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user