agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Website building script should ignore all junk files

Open fredrik-bakke opened this issue 2 years ago • 0 comments

Similar to #664. To fix this, custom.js should probably use .gitignore to filter files.

fredrik-bakke avatar Jun 22 '23 11:06 fredrik-bakke