fix: don't build Lean files twice

PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.

Apache License 2.0

136 stars 23 forks source link

fix: don't build Lean files twice #28

Open fpvandoorn opened 2 weeks ago

fpvandoorn commented 2 weeks ago

Under the setup before this PR, lake builds the Lean files in both the Build project and Build documentation steps, since they use different configuraions.

Compare the build times of "build documentation" before and after this change.