Remove un-needed scripts

[tatoo.git] / tools / osort.sh

diff --git a/tools/osort.sh b/tools/osort.sh
deleted file mode 100755 (executable)
index b967ee3..0000000
--- a/tools/osort.sh
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/sh
-
-EXT="$1"
-if [ -z "$EXT" ]
-then
-    EXT="cmx"
-fi
-
-TARGET="$2"
-
-DEPS=$(
-while read target deps
-do
-    target="${target%.ml:}.$EXT"
-    dir=$(dirname "$target")
-    echo -n "$target":" "
-    for d in $deps
-    do
-        base=$(echo "$d" | sed 's/\(.*\)/\l\1/g' )
-        if [ -f "$dir"/"$base".ml -o -d "$dir"/"$base" ]
-        then
-            echo -n "$dir"/"$base"".$EXT "
-        fi
-    done
-    echo
-done)
-
-SORTED=""
-while true
-do
-    ROOT=$(echo "$DEPS" | grep '^[^ ]*.'$EXT': *$' | cut -f 1 -d: )
-    NDEPS=$(echo "$DEPS" | grep -v '^[^ ]*.'$EXT': *$')
-    if [ "$DEPS" = "$NDEPS" ]
-    then
-        SORTED="$SORTED $(echo $DEPS | cut -f 2 -d :)"
-        SORTED="$SORTED $(echo $DEPS | cut -f 1 -d :)"
-        break
-    fi
-    SORTED="$SORTED $ROOT"
-    for r in $ROOT
-    do
-        DEPS=$(echo "$DEPS" | sed "s|$r:\?||g")
-    done
-done
-for i in $SORTED
-do
-echo -n "$i "
-done
-echo