tools/osort.sh

   1 #!/bin/sh
   2
   3 EXT="$1"
   4 if [ -z "$EXT" ]
   5 then
   6     EXT="cmx"
   7 fi
   8
   9 TARGET="$2"
  10
  11 DEPS=$(
  12 while read target deps
  13 do
  14     target="${target%.ml:}.$EXT"
  15     dir=$(dirname "$target")
  16     echo -n "$target":" "
  17     for d in $deps
  18     do
  19         base=$(echo "$d" | sed 's/\(.*\)/\l\1/g' )
  20         if [ -f "$dir"/"$base".ml -o -d "$dir"/"$base" ]
  21         then
  22             echo -n "$dir"/"$base"".$EXT "
  23         fi
  24     done
  25     echo
  26 done)
  27
  28 SORTED=""
  29 while true
  30 do
  31     ROOT=$(echo "$DEPS" | grep '^[^ ]*.'$EXT': *$' | cut -f 1 -d: )
  32     NDEPS=$(echo "$DEPS" | grep -v '^[^ ]*.'$EXT': *$')
  33     if [ "$DEPS" = "$NDEPS" ]
  34     then
  35         SORTED="$SORTED $(echo $DEPS | cut -f 2 -d :)"
  36         SORTED="$SORTED $(echo $DEPS | cut -f 1 -d :)"
  37         break
  38     fi
  39     SORTED="$SORTED $ROOT"
  40     for r in $ROOT
  41     do
  42         DEPS=$(echo "$DEPS" | sed "s|$r:\?||g")
  43     done
  44 done
  45 for i in $SORTED
  46 do
  47 echo -n "$i "
  48 done
  49 echo