From 1de8526e0c264974523c3c8043ee55965d507902 Mon Sep 17 00:00:00 2001 From: "Kartik K. Agaram" Date: Sat, 30 Oct 2021 12:11:47 -0700 Subject: [PATCH] . --- tools/update_signatures | 1 + 1 file changed, 1 insertion(+) create mode 100755 tools/update_signatures 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