Commit e857acd3 authored by Ralf Jung's avatar Ralf Jung

add issue template

parent 0655aa19
Pipeline #14568 passed with stage
in 20 minutes and 59 seconds
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
  • Cannot we set this as the default issue template; now people have to explicit select "Bug" for this to appear in their issue.

    For another Gitlab I can do that via "Settings > General > Issue settings", but for the Iris Gitlab this feature appears to be missing.

  • Unfortunately this is a Gitlab-EE-only feature. GitLab offers the (usually expensive) EE for free when you do teaching, but we asked and MPI is not eligible because we are mainly a research institute, not a teaching institute.

  • That explains, I saw this feature at the TUDelft Gitlab, which has the enterprise teaching license.

    PS: It's really stupid that Gitlab is putting such minor features only in the enterprise edition...

Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment