From e6276088107e814bea95aee42868065dc41c1e8b Mon Sep 17 00:00:00 2001
From: Frans Kaashoek <kaashoek@mit.edu>
Date: Wed, 24 Jul 2019 09:05:05 -0400
Subject: Delete a few other no-longer relevant files

---
 spinp | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100755 spinp

(limited to 'spinp')

diff --git a/spinp b/spinp
deleted file mode 100755
index db9614b..0000000
--- a/spinp
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/bin/sh
-
-if [ $# != 1 ] || [ ! -f "$1" ]; then
-	echo 'usage: spinp file.p' 1>&2
-	exit 1
-fi
-
-rm -f $1.trail
-spin -a $1 || exit 1
-cc -DSAFETY -DREACH -DMEMLIM=500 -o pan pan.c
-pan -i
-rm pan.* pan
-if [ -f $1.trail ]; then
-	spin -t -p $1
-fi
-
-- 
cgit v1.2.3