Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use plutusrequiredspace where plutusrequiredtime was used mistakenly. #2902

Merged
merged 1 commit into from
Jul 8, 2021
Merged

Use plutusrequiredspace where plutusrequiredtime was used mistakenly. #2902

merged 1 commit into from
Jul 8, 2021

Conversation

newhoggy
Copy link
Contributor

@newhoggy newhoggy commented Jul 7, 2021

No description provided.

Jimbo4350
Jimbo4350 approved these changes Jul 7, 2021
View reviewed changes
Copy link
Contributor

@Jimbo4350 Jimbo4350 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

@newhoggy
Copy link
Contributor Author

newhoggy commented Jul 8, 2021

bors merge

iohk-bors bot added a commit that referenced this pull request Jul 8, 2021
@iohk-bors @newhoggy
Merge #2902
c6116b5 
2902: Use plutusrequiredspace where plutusrequiredtime was used mistakenly. r=newhoggy a=newhoggy



Co-authored-by: John Ky <john.ky@iohk.io>
@iohk-bors
Copy link
Contributor

iohk-bors bot commented Jul 8, 2021

Canceled.

deepfire
deepfire approved these changes Jul 8, 2021
View reviewed changes
Copy link
Contributor

@deepfire deepfire left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@deepfire
Copy link
Contributor

deepfire commented Jul 8, 2021

bors r+

@iohk-bors
Copy link
Contributor

iohk-bors bot commented Jul 8, 2021

Build succeeded:

@iohk-bors iohk-bors bot merged commit 0f18ee4 into master Jul 8, 2021
@iohk-bors iohk-bors bot deleted the use-plutusrequiredspace branch July 8, 2021 04:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Jimbo4350 Jimbo4350 Jimbo4350 approved these changes

@deepfire deepfire deepfire approved these changes

@DavidEichmann DavidEichmann Awaiting requested review from DavidEichmann

@dcoutts dcoutts Awaiting requested review from dcoutts

@erikd erikd Awaiting requested review from erikd

@denisshevchenko denisshevchenko Awaiting requested review from denisshevchenko

@jutaro jutaro Awaiting requested review from jutaro

@MarcFontaine MarcFontaine Awaiting requested review from MarcFontaine

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@newhoggy @deepfire @Jimbo4350