diff options
| -rwxr-xr-x | tools/update_signatures | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/update_signatures b/tools/update_signatures new file mode 100755 index 00000000..4142c835 --- /dev/null +++ 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 |