From 3ca227f1137e6a3b65bc33f5689e1c230d591595 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Tue, 8 Jan 2019 04:21:38 -0500
Subject: remove old pipeline

---
 extract-function-header.sh | 41 -----------------------------------------
 1 file changed, 41 deletions(-)
 delete mode 100755 extract-function-header.sh

(limited to 'extract-function-header.sh')

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
-- 
cgit v1.2.3