Skip to content

GitLab

Switch branch/tag
  1. 02 Sep, 2020 2 commits
  3. 12 Aug, 2020 3 commits
  5. 28 Jul, 2020 2 commits
  7. 27 Jul, 2020 5 commits
  9. 24 Jul, 2020 1 commit
  11. 22 Jul, 2020 1 commit
  13. 20 Jul, 2020 1 commit
  15. 09 Jul, 2020 1 commit
  17. 19 Jun, 2020 2 commits
  19. 27 May, 2020 2 commits
    • Mattia Mancini's avatar
      Merge branch 'spider' into 'master' · d42a2587
      Mattia Mancini authored 
      merge Spider into master

See merge request !1
      d42a2587
    • Leah Morabito's avatar
      Add small modifications to make the merge with the master possible · a35207e9
      Leah Morabito authored 
      Merge branches before making minor changes (e.g., updating json files / repo to deal with spider issue #1) so this doesn't have to be done twice. In particular:
- Switch to more flexible PICAS_API_VERSION selection
- Removing the automatically prepended "v" should allow usage of arbitrary branches. Note this needs to be reflected in the json configuration files as well by e.g. changing "0.5" to "v0.5"
- Minor refactoring
      a35207e9
  21. 28 Oct, 2019 1 commit
  23. 25 Oct, 2019 6 commits
  25. 24 Oct, 2019 13 commits