if test \( "$INTER" = "1" \) -a \( -f "$base".mli \) ; then
## if we want to depend only on cmi of a module
echo -n "$base"."cmi "
if test \( "$INTER" = "1" \) -a \( -f "$base".mli \) ; then
## if we want to depend only on cmi of a module
echo -n "$base"."cmi "