.

2021-10-30 12:11:47 -07:00 · 2021-10-30 12:11:47 -07:00 · 1de8526e0c
parent a69248b284
commit 1de8526e0c
1 changed files with 1 additions and 0 deletions
--- a/tools/update_signatures
+++ b/tools/update_signatures
@ -0,0 +1 @@
+grep -h '^sig \|^fn ' [0-9]*.mu |grep -v 'fn test-' |sed 's/^fn /sig /' |sed 's/ {$//' > signatures.mu
				`@ -0,0 +1 @@`
				`grep -h '^sig \\|^fn ' [0-9]*.mu \|grep -v 'fn test-' \|sed 's/^fn /sig /' \|sed 's/ {$//' > signatures.mu`