You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There is a scriptcount-agda-files-and-lines which I suggest everybody should run before their pull requests, and then update index.lagda with this information.
Specifically, the snippet
* In our last count, on 2024.06.19, this development has 761 Agda
files with 215k lines of code, including comments and blank
lines. But we don't update the count frequently.
should perhaps always be updated in any pull request.
It would be even better if there was an automatic way of doing this.
Then we could omit "But we don't update the count frequently.".
The text was updated successfully, but these errors were encountered:
There is a script
count-agda-files-and-lines
which I suggest everybody should run before their pull requests, and then updateindex.lagda
with this information.Specifically, the snippet
should perhaps always be updated in any pull request.
It would be even better if there was an automatic way of doing this.
Then we could omit "But we don't update the count frequently.".
The text was updated successfully, but these errors were encountered: