Labels

• "bug" :bug:

  "bug" 🐛

  This issue (resp. PR) describes (resp. fixes) a "bug"

• build/continuous integration :gear:

  build/continuous integration ⚙️

  This issue/PR is about the build process or CI

• change MathComp

  change MathComp

  This issue/PR involves a change in the core mathcomp repository

• documentation :memo:

  documentation 📝

  This issue/PR is about documentation of the library / repository

• emergency :ambulance:

  emergency 🚑

  This must be fixed ASAP

• enhancement :sparkles:

  enhancement ✨

  This issue/PR is about adding new features enhancing the library

• experiment :test_tube:

  experiment 🧪

  This issue/PR is very experimental

• good first issue

  good first issue

  This should be a problem easy to tackle by a beginner

• help :sos:

  help 🆘

  This author/reviewer of this issue/PR needs external help

• needs: drop 8.20

  needs: drop 8.20

• packaging/releasing

  packaging/releasing

  Issue/PR about packaging or realising.

• question :question:

  question ❓

  There is an unanswered question here

• renaming/refactoring :wrench:

  renaming/refactoring 🔧

  This is about a renaming or refactoring in the library

• TODO: MC2 port

  TODO: MC2 port

  This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.

• wish :pray:

  wish 🙏

  Request for a specific mathematical result

• wontfix/merge :no_entry_sign:

  wontfix/merge 🚫

  We wont fix this issue/merge this PR, we will close it soon