phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

make command line look the same on all browsers

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-02-09 13:43:59 +01:00
parent 6e8a47b1a7
commit ca329a933c
1 changed files with 5 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/infoview.css
+5 -2
View File
@@ -48,8 +48,9 @@
display: flex; display: flex;
} }
.command-line form>input{ .command-line button {
display: block; display: block;
white-space: nowrap;
} }
.command-line .command-line-input-wrapper{ .command-line .command-line-input-wrapper{
@@ -57,10 +58,12 @@
padding: 0.4em .6em 0; padding: 0.4em .6em 0;
font-size: 1rem; font-size: 1rem;
background: white; background: white;
display: flex;
flex-direction: column;
} }
.command-line .command-line-input{ .command-line .command-line-input{
height: 1.2em; flex: 1;
} }
/* Turn off some monaco decorations: */ /* Turn off some monaco decorations: */