Skip to content

Conversation

Ailrun
Copy link
Member

@Ailrun Ailrun commented Feb 16, 2021

Before this PR, the script creates ([PR number)](link), which makes ) after the PR number also clickable. This PR fixes so that only the PR number is treated as a link.

@Ailrun
Copy link
Member Author

Ailrun commented Feb 17, 2021

BTW: do we even need to check CI for PR like this?

@berberman
Copy link
Collaborator

For github actions, we could use paths or paths-ignore to configure files we don't want to trigger CI on update.

@jneira
Copy link
Member

jneira commented Feb 17, 2021

yeah I want to add it and maybe honour the tag ci skip since some time ago 😅

Copy link
Member

@jneira jneira left a comment

Choose a reason for hiding this comment

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

thanks for the fix, maybe we should correct existing entries? (maybe in the next release)

@Ailrun
Copy link
Member Author

Ailrun commented Feb 17, 2021

@Ailrun Ailrun added the merge me Label to trigger pull request merge label Feb 17, 2021
@jneira
Copy link
Member

jneira commented Feb 17, 2021

oh sorry I missed it in the mobile app UI

@mergify mergify bot merged commit 240f793 into haskell:master Feb 18, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge me Label to trigger pull request merge

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants