Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

update line and file count #290

Open
martinescardo opened this issue Jun 23, 2024 · 1 comment
Open

update line and file count #290

martinescardo opened this issue Jun 23, 2024 · 1 comment

Comments

@martinescardo
Copy link
Owner

martinescardo commented Jun 23, 2024

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.".

@ayberkt
Copy link
Collaborator

ayberkt commented Jun 23, 2024

It would be even better if there was an automatic way of doing this.

It is possible to automate it and I would be happy to implement it. It should be relatively easy to do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants