diff --git a/install b/install index 9c283df..89d5247 100755 --- a/install +++ b/install @@ -98,7 +98,7 @@ check_afp_entries() { if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then for e in $missing; do echo " Registering $e in $ISABELLE_HOME_USER/ROOTS" - echo "$PWD/.afp/afp-2018-08-14/thys/$e" >> $ISABELLE_HOME_USER/ROOTS + grep -q $PWD/.afp/afp-2018-08-14/thys/$e || echo "$PWD/.afp/afp-2018-08-14/thys/$e" >> $ISABELLE_HOME_USER/ROOTS done echo " AFP installation successful." else