remove old pipeline

1 files changed, 0 insertions, 41 deletions

diff --git a/extract-function-header.sh b/extract-function-header.sh
deleted file mode 100755
index 36676db06..000000000
--- a/extract-function-header.sh
+++ /dev/null
@@ -1,41 +0,0 @@
-#!/bin/sh
-set -eu
-
-case "$#" in
-  0)
-    funcname=f
-    ;;
-  1)
-    funcname="$1"
-    ;;
-  *)
-    exit 111
-    ;;
-esac
-
-cat <<"EOF"
-#include <stdint.h>
-
-#undef force_inline
-#define force_inline __attribute__((always_inline))
-
-EOF
-
-if [ -z "${BITWIDTH}" ]; then
-  BITWIDTH=64
-fi
-
-while IFS= read -r line; do
-  case "$line" in
-    *"λ '"*)
-      echo -n "void force_inline $funcname("
-      echo -n "uint${BITWIDTH}_t* out"
-      echo "$line" | grep -owP -- '\w+\d+' | \
-        while IFS= read -r arg; do
-          echo -n ", uint${BITWIDTH}_t $arg"
-        done
-        echo ');'
-      break
-      ;;
-  esac
-done