Skip to content

Actions: mhuisi/vscode-lean4

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
17 workflow runs
17 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: improve Markdown popup rendering (#534)
vscode-lean4 build #17: Commit cd70bdd pushed by mhuisi
October 17, 2024 16:42 6m 54s master
October 17, 2024 16:42 6m 54s
Release 0.0.177
vscode-lean4 build #16: Commit 97d7d8c pushed by mhuisi
August 30, 2024 14:37 5m 40s master
August 30, 2024 14:37 5m 40s
fix: allow downloading projects with ssh git links (#386)
vscode-lean4 build #15: Commit 72d7062 pushed by mhuisi
January 15, 2024 12:30 6m 31s master
January 15, 2024 12:30 6m 31s
feat: customizable occurrence highlighting (#377)
vscode-lean4 build #14: Commit ceccfe7 pushed by mhuisi
January 9, 2024 09:08 6m 10s master
January 9, 2024 09:08 6m 10s
feat: optional user widget names (#376)
vscode-lean4 build #13: Commit a09d19a pushed by mhuisi
December 22, 2023 14:23 3m 52s master
December 22, 2023 14:23 3m 52s
Release 0.0.121
vscode-lean4 build #12: Commit 063edd1 pushed by mhuisi
November 27, 2023 15:27 6m 15s master
November 27, 2023 15:27 6m 15s
Release 0.0.120
vscode-lean4 build #11: Commit 61b60a5 pushed by mhuisi
November 27, 2023 13:34 6m 12s master
November 27, 2023 13:34 6m 12s
chore: add rrbracket to abbreviations (#360)
vscode-lean4 build #10: Commit 08d46f1 pushed by mhuisi
November 22, 2023 11:07 7m 24s master
November 22, 2023 11:07 7m 24s
Release 0.0.119
vscode-lean4 build #9: Commit 8d0cc34 pushed by mhuisi
November 21, 2023 12:34 6m 48s master
November 21, 2023 12:34 6m 48s
fix: update semver (#343)
vscode-lean4 build #8: Commit 3f62c2a pushed by mhuisi
November 16, 2023 09:14 6m 18s master
November 16, 2023 09:14 6m 18s
fix: still start language client when project folder is invalid
vscode-lean4 build #7: Commit a5e1034 pushed by mhuisi
November 10, 2023 15:04 6m 51s master
November 10, 2023 15:04 6m 51s
Release 0.0.118
vscode-lean4 build #6: Commit 2f3f44e pushed by mhuisi
November 2, 2023 09:36 6m 23s master
November 2, 2023 09:36 6m 23s
fix: bad error message + crash without default toolchain
vscode-lean4 build #5: Commit 76ccd1d pushed by mhuisi
October 31, 2023 17:11 10m 12s master
October 31, 2023 17:11 10m 12s
chore: change name of 'create mathlib project' command
vscode-lean4 build #4: Commit b023be4 pushed by mhuisi
October 31, 2023 15:09 9m 33s master
October 31, 2023 15:09 9m 33s
Release 0.0.117
vscode-lean4 build #3: Commit a79d9b4 pushed by mhuisi
October 30, 2023 12:32 9m 36s master
October 30, 2023 12:32 9m 36s
Release 0.0.116 (pre-release)
vscode-lean4 build #2: Commit 0e98f2e pushed by mhuisi
October 18, 2023 13:33 4m 59s master
October 18, 2023 13:33 4m 59s
Release 0.0.115 (pre-release)
vscode-lean4 build #1: Commit 71e67ad pushed by mhuisi
October 18, 2023 12:35 4m 39s master
October 18, 2023 12:35 4m 39s