From a4ad260a719d9dbb6d8218f2728bed804857ad30 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jesper=20=C3=96qvist?= <jesper.oqvist@cs.lth.se>
Date: Mon, 19 Aug 2013 13:12:12 +0200
Subject: [PATCH] Publish index.md rather than index.html in release
The index.html file is rendered instead of index.php which means that
the menu is missing because header/footer html is not rendered.
Publishing index.md instead fixes this problem.
---
doc/index.php | 2 +-
release.sh | 11 +++++++++--
2 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/doc/index.php b/doc/index.php
index 02c2e23f..8738ce7f 100644
--- a/doc/index.php
+++ b/doc/index.php
@@ -1,4 +1,4 @@
<?php
include("../../../web/include/functions.php");
-printHtmlFile("index.html");
+printMarkdownFile("index.md");
?>
diff --git a/release.sh b/release.sh
index 1364e097..5e48b929 100755
--- a/release.sh
+++ b/release.sh
@@ -45,8 +45,15 @@ ant release -Dversion=$VERSION
echo "Uploading files to jastadd.org..."
# --chmod=g+w sets group write permission
-rsync -av --chmod=g+w jastadd2-src.zip jastadd2-bin.zip doc/*.html doc/*.php \
- README.md login.cs.lth.se:/cs/jastadd/releases/jastadd2/${VERSION}
+rsync -av --chmod=g+w \
+ jastadd2-src.zip \
+ jastadd2-bin.zip \
+ README.md \
+ doc/*.php \
+ doc/index.md \
+ doc/reference-manual.html \
+ doc/release-notes.html \
+ login.cs.lth.se:/cs/jastadd/releases/jastadd2/${VERSION}
echo
echo "Check that it works!"
--
GitLab