mathlib3
chore(ci): remove unused olean-rs setup from build
#1932

Merged

chore(ci): remove unused olean-rs setup from build #1932

cipher1024 merged 1 commit into master from robertylewis-patch-1

chore(ci): remove unused olean-rs setup from build

30da8e7b

cipher1024 merged cae9cc97 into master 6 years ago

cipher1024 deleted the robertylewis-patch-1 branch 6 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone