Code

Fix deprecated modules#2224

Code

Merged

JacquesCarette merged 4 commits intoagda:masteragda/agda-stdlib:masterfrom

alexarice:deprecated-fixalexarice/agda-stdlib:deprecated-fixCopy head branch name to clipboard

Dec 6, 2023

Commits

Commits on Dec 5, 2023

• Fix deprecated modules

  alexarice

  committed
  19f1c3f

  Copy full SHA for 19f1c3f

• [ ci ] Also build deprecated modules

  gallais

  committed
  8444b99

  Copy full SHA for 8444b99

• [ ci ] ignore user warnings in test

  gallais

  committed
  588ba89

  Copy full SHA for 588ba89

Commits on Dec 6, 2023

• [ ci ] fix filtering logic

  Show description for 7c3b37a
  gallais

  committed
  7c3b37a

  Copy full SHA for 7c3b37a