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.

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

merge various PRs to make CI green again #3371

Merged
merged 6 commits into from
Oct 28, 2018

Commits on Oct 28, 2018

  1. Configuration menu
    Copy the full SHA
    0d89956 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    6eb1f23 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    9a1bb7b View commit details
    Browse the repository at this point in the history
  4. pin compiletest dependency to git version (12c980f47971b5ba6beb7cb2ff…

    …ebf8b32f6766ea) while we are waiting for a new release
    matthiaskrgr committed Oct 28, 2018
    Configuration menu
    Copy the full SHA
    3496975 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    261fe24 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    3f01619 View commit details
    Browse the repository at this point in the history