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

Factor metafiles to a subdirectory

Open fredrik-bakke opened this issue 1 year ago • 0 comments

We have a growing collection of metafiles that are polluting the root folder of the repository. I think it would be best if we moved them to a subdirectory. This would also make them a little more maintainable, as we won't have to maintain a list in the Makefile.

fredrik-bakke avatar Mar 09 '24 20:03 fredrik-bakke