Admin/makebin
changeset 27588 0dd8d4c558f9
parent 27587 6f469a8aff10
child 28504 7ad7d7d6df47
equal deleted inserted replaced
27587:6f469a8aff10 27588:0dd8d4c558f9
   110 
   110 
   111 if [ -n "$DRY_RUN" ]; then
   111 if [ -n "$DRY_RUN" ]; then
   112   mkdir -p "heaps/$COMPILER/log"
   112   mkdir -p "heaps/$COMPILER/log"
   113   touch "heaps/$COMPILER/HOL"
   113   touch "heaps/$COMPILER/HOL"
   114   touch "heaps/$COMPILER/log/HOL.gz"
   114   touch "heaps/$COMPILER/log/HOL.gz"
   115   touch "heaps/$COMPILER/HOL-Complex"
       
   116   touch "heaps/$COMPILER/log/HOL-Complex.gz"
       
   117   touch "heaps/$COMPILER/HOL-Nominal"
   115   touch "heaps/$COMPILER/HOL-Nominal"
   118   touch "heaps/$COMPILER/log/HOL-Nominal.gz"
   116   touch "heaps/$COMPILER/log/HOL-Nominal.gz"
   119   touch "heaps/$COMPILER/ZF"
   117   touch "heaps/$COMPILER/ZF"
   120   touch "heaps/$COMPILER/log/ZF.gz"
   118   touch "heaps/$COMPILER/log/ZF.gz"
   121   mkdir browser_info
   119   mkdir browser_info
   122 elif [ -n "$DO_LIBRARY" ]; then
   120 elif [ -n "$DO_LIBRARY" ]; then
   123   ./build -bait
   121   ./build -bait
   124 else
   122 else
   125   ./build -b -m HOL-Complex HOL
       
   126   ./build -b -m HOL-Nominal HOL
   123   ./build -b -m HOL-Nominal HOL
   127   ./build -b ZF
   124   ./build -b ZF
   128   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   125   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   129 fi
   126 fi
   130 
   127 
   139 if [ -n "$DO_LIBRARY" ]; then
   136 if [ -n "$DO_LIBRARY" ]; then
   140   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   137   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   141     gzip -f "${ISABELLE_NAME}_library.tar"
   138     gzip -f "${ISABELLE_NAME}_library.tar"
   142     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   139     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   143 else
   140 else
   144   for IMG in HOL HOL-Complex HOL-Nominal ZF
   141   for IMG in HOL HOL-Nominal ZF
   145   do
   142   do
   146     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   143     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   147       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   144       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   148       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   145       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   149     gzip -f "${IMG}_$PLATFORM.tar"
   146     gzip -f "${IMG}_$PLATFORM.tar"