Closed Lukires closed 1 year ago
The editor cuts off weirdly off sometimes. I think we need to refresh the editor in the JS after an API call or something like that. I think the problem is when the output is long, it expands the editor div, so we need to refresh the ace editor.
Fixed in https://github.com/diku-dk/futhark-playground/commit/d12ec21bd543f6b81c31fc6483c7b4cbabfe6a97
Lukires
commented
1 year ago
The editor cuts off weirdly off sometimes. I think we need to refresh the editor in the JS after an API call or something like that. I think the problem is when the output is long, it expands the editor div, so we need to refresh the ace editor.