equal
deleted
inserted
replaced
11 <body class="dist"> |
11 <body class="dist"> |
12 <?include file="//include/header.include.html"?> |
12 <?include file="//include/header.include.html"?> |
13 <div class="hr"><hr/></div> |
13 <div class="hr"><hr/></div> |
14 <?include file="//include/navigation_dist.include.html"?> |
14 <?include file="//include/navigation_dist.include.html"?> |
15 <div class="hr"><hr/></div> |
15 <div class="hr"><hr/></div> |
|
16 |
16 <div id="content"> |
17 <div id="content"> |
|
18 <?include file="//include/mirrorlist.minor.include.html"?> |
|
19 <div class="hr"><hr/></div> |
|
20 |
17 <h2>Welcome to the Isabelle Distribution!</h2> |
21 <h2>Welcome to the Isabelle Distribution!</h2> |
18 |
22 |
19 <p>First, you might like to switch to a nearby mirror:</p> |
23 <p>First, you might like to switch to a nearby mirror:</p> |
20 |
24 |
21 <ul> |
25 <ul> |