Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: deps-order.sh Sprache: Shell

Original von: Coq^©

#!/bin/sh
# Check that both coqdep and coqtop/coqc supports -R
# Check that both coqdep and coqtop/coqc takes the later -R
# See bugs 2242, 2337, 2339
rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX)
$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$tmpoutput"
diff -u --strip-trailing-cr misc/deps/deps.out "$tmpoutput" 2>&1
R=$?
times
$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1
S=$?
if [ $R = 0 ] && [ $S = 0 ]; then
    printf "coqdep and coqc agree\n"
    exit 0
else
    printf "coqdep and coqc disagree\n"
    exit 1
fi

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.