Set `default-toolchain` to `none`

PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.

Apache License 2.0

170 stars 28 forks source link

Closed pitmonticone closed 3 months ago

pitmonticone commented 3 months ago

This PR sets default-toolchain to none.

Projects using this config:

pitmonticone commented 3 months ago

I'm going to close it since it would be "generalised" in the next PR