Code

Introduce package "notices"#320

Code

Merged

stefan-hoeck merged 2 commits intostefan-hoeck:mainstefan-hoeck/idris2-pack:mainfrom mattpolzin:introduce-notice-configmattpolzin/idris2-pack:introduce-notice-configCopy head branch name to clipboardJan 19, 2025

+41-30

Commits

Commits on Jan 17, 2025

• Add notice config option

  mattpolzin

  committed
  e7d7f83

  Copy full SHA for e7d7f83

Commits on Jan 18, 2025

• expose any given notice as a warning when installing a package.

  mattpolzin

  committed
  e0b05e6

  Copy full SHA for e0b05e6