12 while read target deps
14 target="${target%.ml:}.$EXT"
15 dir=$(dirname "$target")
19 base=$(echo "$d" | sed 's/\(.*\)/\l\1/g' )
20 if [ -f "$dir"/"$base".ml -o -d "$dir"/"$base" ]
22 echo -n "$dir"/"$base"".$EXT "
31 ROOT=$(echo "$DEPS" | grep '^[^ ]*.'$EXT': *$' | cut -f 1 -d: )
32 NDEPS=$(echo "$DEPS" | grep -v '^[^ ]*.'$EXT': *$')
33 if [ "$DEPS" = "$NDEPS" ]
35 SORTED="$SORTED $(echo $DEPS | cut -f 2 -d :)"
36 SORTED="$SORTED $(echo $DEPS | cut -f 1 -d :)"
39 SORTED="$SORTED $ROOT"
42 DEPS=$(echo "$DEPS" | sed "s|$r:\?||g")