diff options
author | stuebinm | 2022-03-06 18:13:08 +0100 |
---|---|---|
committer | stuebinm | 2022-03-06 18:13:08 +0100 |
commit | 6b71528e72458bcb5e0a0089033b9367c887967f (patch) | |
tree | 558b0df9b4760fd8712b35aea4910e8d62330483 /server | |
parent | c79dd30b1e335a536df80d0e60b0bca8c9dc5141 (diff) |
server: small html improvementsplayground
bootstrap is horrible and should be replaced
Diffstat (limited to 'server')
-rw-r--r-- | server/HtmlOrphans.hs | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/server/HtmlOrphans.hs b/server/HtmlOrphans.hs index ee30773..64de2f6 100644 --- a/server/HtmlOrphans.hs +++ b/server/HtmlOrphans.hs @@ -55,9 +55,11 @@ instance ToHtml JobStatus where autoReloadScript Linted res _rev (pending, _) -> do h1_ "Linter Result" - if pending - then button_ [class_ "btn btn-primary btn-disabled", disabled_ "true"] "pending …" - else button_ [onclick_ "relint()", class_ "btn btn-primary", id_ "relint_button"] "relint" + p_ $ do + "your map will be re-linted periodically. " + if pending + then button_ [class_ "btn btn-primary btn-disabled", disabled_ "true"] "pending …" + else button_ [onclick_ "relint()", class_ "btn btn-primary", id_ "relint_button"] "relint now" toHtml res script_ "function relint() {\n\ @@ -147,6 +149,7 @@ instance ToHtml (DirResult a) where unless (null dirresultDeps) $ ul_ $ forM_ dirresultDeps $ \missing -> do li_ $ do + " " -- TODO: the whole Maybe Bool thing is annoying; I think that was a -- remnant of talking to python stuff and can probably be removed? if depFatal missing == Just True |