[Merged by Bors] - chore: remove the ProofWidgets import#11877

Closed

eric-wieser wants to merge 3 commits intomasterfrom

eric-wieser/remove-ProofWidgets-import

Member

eric-wieser commented Apr 3, 2024 •

edited

Loading

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import ProofWidgets.Demos.*, and any other auxiliary content in upstream packages that is not part of the top-level package.


          remove the ProofWidgets import

75203b1

eric-wieser added awaiting-review awaiting-CI labels

eric-wieser changed the title ~~remove the ProofWidgets import~~ chore: remove the ProofWidgets import

eric-wieser added 2 commits

April 3, 2024 23:57


          fix makefile

ec27bbc


          tidy

48cad2c

eric-wieser requested a review from digama0

April 4, 2024 00:02

github-actions bot removed the awaiting-CI label

digama0 approved these changes

View reviewed changes

Contributor

kim-em commented Apr 4, 2024

bors merge

github-actions bot added ready-to-merge and removed awaiting-review labels

mathlib-bors bot pushed a commit that referenced this pull request


          chore: remove the ProofWidgets import (#11877)

e545009

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package.

Contributor

mathlib-bors bot commented Apr 4, 2024

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~chore: remove the ProofWidgets import~~ [Merged by Bors] - chore: remove the ProofWidgets import

mathlib-bors bot closed this

mathlib-bors bot deleted the eric-wieser/remove-ProofWidgets-import branch

April 4, 2024 08:32

xgenereux pushed a commit that referenced this pull request


          chore: remove the ProofWidgets import (#11877)

deeed69

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package.

atarnoam pushed a commit that referenced this pull request


          chore: remove the ProofWidgets import (#11877)

669ad32

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package.

uniwuni pushed a commit that referenced this pull request


          chore: remove the ProofWidgets import (#11877)

80f6ba7

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package.

callesonne pushed a commit that referenced this pull request


          chore: remove the ProofWidgets import (#11877)

0513b4e

This follows on from #11350, following an alternative suggestion by @digama0.

One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package.

eric-wieser added a commit that referenced this pull request


          fix: undo the accidental revert of #11877 in #11807

c495a86

A bad merge in #11807 causes the change from #11877 to be reverted.

eric-wieser mentioned this pull request

[Merged by Bors] - fix: undo the accidental revert of #11877 in #11807 #15523

Closed

mathlib-bors bot pushed a commit that referenced this pull request


          fix: undo the accidental revert of #11877 in #11807 (#15523)

1d4f2c1

A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted.

bjoernkjoshanssen pushed a commit that referenced this pull request


          fix: undo the accidental revert of #11877 in #11807 (#15523)

01c5e38

A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted.

bjoernkjoshanssen pushed a commit that referenced this pull request


          fix: undo the accidental revert of #11877 in #11807 (#15523)

ffb0693

A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted.

bjoernkjoshanssen pushed a commit that referenced this pull request


          fix: undo the accidental revert of #11877 in #11807 (#15523)

a81a323

A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels