Skip to content
Snippets Groups Projects
Select Git revision
  • e7d35ace2b41f827b51059e46606d7686166e1cd
  • master default protected
2 results

rodin_handbook

  • Open with
  • Download source code
  • Your workspaces

      A workspace is a virtual sandbox environment for your code in GitLab.

      No agents available to create workspaces. Please consult Workspaces documentation for troubleshooting.

    • user avatar
    Switch from Travis CI to GitLab CI
    dgelessus authored 
    Using the very Ubuntu 14.04 (trusty) for now, because that's the closest
match to what Travis CI had at the time. Unfortunately, this build needs
a very particular combination of old package versions.
    e7d35ace
    History
    user avatar e7d35ace
    History
    Name Last commit Last update