X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=tools%2Fosort.sh;fp=tools%2Fosort.sh;h=b967ee3924c9186be6e7cf8a2d72f6efee3b8b15;hp=0000000000000000000000000000000000000000;hb=8af68de11421dacc2f77a8398dcb48c75a5ff3b1;hpb=9efb3171eb9f70c92d7814a56684ef5f1eedf004

diff --git a/tools/osort.sh b/tools/osort.sh
new file mode 100755
index 0000000..b967ee3
--- /dev/null
+++ b/tools/osort.sh
@@ -0,0 +1,49 @@
+#!/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