Skip to content
Build

Replace prerendered banner with logo #66

Sign in to view logs

Replace prerendered banner with logo

Replace prerendered banner with logo #66

Triggered via push October 14, 2024 15:17
@fwcdfwcd
pushed 56a9ae3
main
Status Success
Total duration 16m 34s
Artifacts –

build.yml

on: push
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

6 warnings
build (macos-latest): src/Curry/LanguageServer/Index/Store.hs#L277
The record update def
build (macos-latest): src/Curry/LanguageServer/Handlers/Initialize.hs#L20
Defined but not used: ‘updater’
build (ubuntu-latest): src/Curry/LanguageServer/Index/Store.hs#L277
The record update def
build (ubuntu-latest): src/Curry/LanguageServer/Handlers/Initialize.hs#L20
Defined but not used: ‘updater’
build (windows-latest): src/Curry/LanguageServer/Index/Store.hs#L277
The record update def
build (windows-latest): src/Curry/LanguageServer/Handlers/Initialize.hs#L20
Defined but not used: `updater'