Skip to content

Commit 5e9fe26

Browse files
committed
[ doc ] explain option choice
1 parent 827c2fe commit 5e9fe26

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

stdlib-install.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ logHappy "Agda executable: $AGDA_EXEC"
3030
# Ask the executable for its version number
3131
# unless the caller has specified one
3232
if [ -z ${AGDA_VERSION-} ]; then
33+
# There is a more recent "--numeric-version" option but old
34+
# versions of Agda do not implement it!
3335
AGDA_VERSION=$($AGDA_EXEC --version | head -n 1 | sed "s/^[a-zA-Z ]*\(2[0-9.]*\)\(-.*\)*$/\1/")
3436
fi
3537

0 commit comments

Comments
 (0)