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

Setup GitHub action #44

Merged
merged 3 commits into from
May 12, 2020
Merged

Setup GitHub action #44

merged 3 commits into from
May 12, 2020
+49 −38

Conversation

nkcr
Copy link
Contributor

@nkcr nkcr commented May 12, 2020 •
edited
Loading

I wanted to give GitHub action a try, and I see many advantages using it:

  • More concurrent jobs available
  • Offers a nice text editor that shows syntax error and help
  • Allows to have separate jobs with separate badges
  • Better interface to follow jobs status and error

@nkcr nkcr self-assigned this May 12, 2020
@nkcr nkcr requested a review from Gilthoniel May 12, 2020 15:52
@Gilthoniel Gilthoniel merged commit d1864da into master May 12, 2020
@Gilthoniel Gilthoniel deleted the nkcr-patch-2 branch May 12, 2020 18:44
bbjubjub2494 pushed a commit to bbjubjub2494/dela that referenced this pull request Aug 3, 2024
Merge pull request dedis#44 from dedis/nkcr-patch-2
8db496b 
Setup GitHub action
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Gilthoniel Gilthoniel Awaiting requested review from Gilthoniel

Assignees

@nkcr nkcr

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nkcr @Gilthoniel