Admin/make_everything
changeset 12721 226fc0e2e7e3
parent 11121 44db3b518ca2
child 16301 f9f2e1643593
equal deleted inserted replaced
12720:f8a134b9a57f 12721:226fc0e2e7e3
     1 #!/bin/bash
     1 #!/usr/bin/env bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # make_everything -- an adhoc script that demonstrates the general procedure
     5 # make_everything -- an adhoc script that demonstrates the general procedure
     6 #   of creating the Isabelle distribution and WWW page
     6 #   of creating the Isabelle distribution and WWW page