Skip to content

Commit

Permalink
Add a script for updating the file and line count
Browse files Browse the repository at this point in the history
  • Loading branch information
ayberkt committed Jul 16, 2024
1 parent aada603 commit 128d3f8
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions updatecount
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#!/bin/bash

input_file="source/index.lagda"

current_date=$(date +"%Y.%m.%d")

file_count=$(git ls-files source | grep agda | wc -l | xargs)
line_count=$(git ls-files source | grep agda | xargs cat | wc -l | xargs | awk '{printf "%.0fK\n", $1/1000}')

echo "File count is $file_count."
echo "Line count is $line_count."

sed -i '' "s/In our last count, on [0-9.]\{1,\},/In our last count, on $current_date,/g" $input_file
sed -i '' "s/this development has [0-9]\{1,\} Agda/this development has $file_count Agda/g" $input_file
sed -i '' "s/files with [0-9kK]\{1,\} lines of code/files with $line_count lines of code/g" $input_file

0 comments on commit 128d3f8

Please sign in to comment.