Skip to content

[Merged by Bors] - fix: remove custom applicationTime from simps#1958

Closed
fpvandoorn wants to merge 2 commits intomasterfrom
removeapplicationtime
Closed

[Merged by Bors] - fix: remove custom applicationTime from simps#1958
fpvandoorn wants to merge 2 commits intomasterfrom
removeapplicationtime

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jan 30, 2023

This should not matter anymore after #1314

  • I tried removing it from to_additive, but that fails, presumably because to_additive has to be able to add other attributes, like simp.

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 30, 2023
@fpvandoorn fpvandoorn changed the title fix: remove custom applicationTime from to_additive and simps fix: remove custom applicationTime from simps Jan 31, 2023
@fpvandoorn fpvandoorn added easy < 20s of review time. See the lifecycle page for guidelines. and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 31, 2023
@gebner
Copy link
Copy Markdown
Member

gebner commented Jan 31, 2023

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 31, 2023
bors bot pushed a commit that referenced this pull request Jan 31, 2023
This should not matter anymore after #1314 

* I tried removing it from `to_additive`, but that fails, presumably because `to_additive` has to be able to add other attributes, like `simp`.
@bors
Copy link
Copy Markdown

bors bot commented Jan 31, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix: remove custom applicationTime from simps [Merged by Bors] - fix: remove custom applicationTime from simps Jan 31, 2023
@bors bors bot closed this Jan 31, 2023
@bors bors bot deleted the removeapplicationtime branch January 31, 2023 19:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants