Code

README.Data.* manual fix for #1380#2285

Code

Merged

MatthewDaggitt merged 1 commit intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:defunct-READMEsjamesmckinna/agda-stdlib:defunct-READMEsCopy head branch name to clipboardFeb 14, 2024

Commits

Commits on Feb 8, 2024

• manual fix for agda#1380

  jamesmckinna

  committed
  200e00d

  Copy full SHA for 200e00d