Bug fix: create .afp directory if it does not exist.

2019-01-08 09:36:11 +00:00 · 2019-01-08 09:36:11 +00:00 · 209c9aaca8
parent 843617ed2a
commit 209c9aaca8
1 changed files with 1 additions and 0 deletions
--- a/1
+++ b/1
@ -94,6 +94,7 @@ check_afp_entries() {
 	for e in $missing; do
 	    extract="$extract afp-2018-08-14/thys/$e"
 	done
+	mkdir -p .afp
        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"