search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Version compatible to stdlib 1.7 and agda 2.6.2 #288

Closed Akshobhya1234 closed 3 years ago

Akshobhya1234 commented 3 years ago

PR changing the CI variable to use 2.6.2 and 1.7 Issue #287

ice1000 commented 3 years ago

image

GitHub is not showing you as the author of these commits. Maybe you should reconfigure your email settings.

ice1000 commented 3 years ago

Let's run the GitHub workflow

Akshobhya1234 commented 3 years ago

image

GitHub is not showing you as the author of these commits. Maybe you should reconfigure your email settings.

"akshobhya.k.m@sap.com" is my enterprise account. "Akshobhya1234" is my personal account. My local is setup for enterprise account and I have forked the repo to my personal account.

ice1000 commented 3 years ago

GitHub is not showing you as the author of these commits. Maybe you should reconfigure your email settings.

"akshobhya.k.m@sap.com" is my enterprise account. "Akshobhya1234" is my personal account. My local is setup for enterprise account and I have forked the repo to my personal account.

I totally understand the reason why this happens. I'm just saying that by doing this, GitHub will not count you, the user @Akshobhya1234, as a contributor to this project.

Akshobhya1234 commented 3 years ago

GitHub is not showing you as the author of these commits. Maybe you should reconfigure your email settings.

"akshobhya.k.m@sap.com" is my enterprise account. "Akshobhya1234" is my personal account. My local is setup for enterprise account and I have forked the repo to my personal account.

I totally understand the reason why this happens. I'm just saying that by doing this, GitHub will not count you, the user @Akshobhya1234, as a contributor to this project.

Yes. But once this PR is merged I think it will consider with @Akshobhya1234 as contributor ( based on merge commit). It is fine for me if GitHub doesn't count me as contributor as long as it is fine with the team.

ice1000 commented 3 years ago

@gallais merge?

JacquesCarette commented 3 years ago

Thanks, merged. I'm going to wait for the build to finish to make a release.