fix: public import to get olean in cache

7043432

Select commit

Loading

Failed to load commit list.

There was an error while loading. Please reload this page.

Clean Dependabot PR descriptions on: pull_request

clean-description

actionlint

Check for copyright header and too-big Lean imports on: pull_request 1

Check copyright header and Lean import size

Lint GitHub Actions workflows on: pull_request 1

Lint GitHub Actions workflows

Check toolchain file on: pull_request 1

Check for "nightly" in lean-toolchain

All test modules imported on: pull_request 1

Check all test modules are imported

Continuous Integration on: pull_request

Build and test

Check Code Formatting on: pull_request 2

check-prettier-formatting

check-python-formatting

Check for trailing newlines on: pull_request 1

Check text files have trailing newlines

No tracked ignored files on: pull_request 1

Check no tracked file matches .gitignore

Release note required on: pull_request 1

Check the PR has a release note

Consistent subproject dependencies on: pull_request 1

SubVerso version consistency

Check PR title follows commit convention on: pull_request 1

PR title follows commit convention

No #eval in source files on: pull_request 1

Check no #eval in source files