agda-unimath
agda-unimath copied to clipboard
Website building script should ignore all junk files
Similar to #664. To fix this, custom.js should probably use .gitignore to filter files.