Skip to content
Snippets Groups Projects
Select Git revision
  • 87fa0c5b283b2f572138d92f654f0999e0411bf1
  • develop default protected
  • master protected
  • rodin2
  • rodin3
  • feature/theory_plugin
  • feature/multiview
  • csp
  • feature/newcore
  • feature/csp
  • 3.0.11
  • 3.0.8
  • 3.0.5
  • 2.4.1
  • 2.3.3
  • 2.3.2
  • 2.3.1
  • 2.3.0_fix1
  • 2.3.0
19 results

prob_rodin_plugin

  • Clone with SSH
  • Clone with HTTPS
    • user avatar
    Add category.xml to Git instead of generating it
    dgelessus authored 
    Now that the version numbers no longer need to change, there's no need
to generate this file dynamically anymore.
    87fa0c5b
    History
    user avatar 87fa0c5b
    History
    Name Last commit Last update