diff --git a/Jenkinsfile-publish-doc b/Jenkinsfile-publish-doc
index ea033cd2a..1e61f1376 100644
--- a/Jenkinsfile-publish-doc
+++ b/Jenkinsfile-publish-doc
@@ -8,7 +8,7 @@ node("master") {
}
stage("Producing doc") {
- sh "./scripts/extract_user_doc.sh"
+ sh "./scripts/extract_user_doc.sh -i " + BRANCH_NAME
}
stage("Publish doc") {
diff --git a/scripts/extract_user_doc.rb b/scripts/extract_user_doc.rb
index 9dd53d767..34b6daf56 100755
--- a/scripts/extract_user_doc.rb
+++ b/scripts/extract_user_doc.rb
@@ -24,6 +24,200 @@ def xml2html(t)
end
+title = "KLayout "
+title += (ENV["KLAYOUT_VERSION"] || "$version") + " "
+title += "("
+title += (ENV["KLAYOUT_VERSION_DATE"] || "$date") + " "
+title += (ENV["KLAYOUT_VERSION_REV"] || "$rev")
+title += ") "
+title += ($target_info && $target_info != "" ? "[#{$target_info}] " : "")
+
+HEADER=<<"END"
+
+
+
+
+ KLayout Documentation
+
+
+
+
+#{title}
+END
+
+TAIL=<<"END"
+
+END
+
hs = RBA::HelpSource.new
@@ -34,7 +228,7 @@ hs.urls.each do |url|
fn = ($target_doc + url).sub(/\.xml$/, ".html")
t = hs.get(url)
- t = xml2html(t)
+ t = HEADER + xml2html(t) + TAIL
tt = nil
if File.exists?(fn)
diff --git a/scripts/extract_user_doc.sh b/scripts/extract_user_doc.sh
index 342b4155f..7eadefeb3 100755
--- a/scripts/extract_user_doc.sh
+++ b/scripts/extract_user_doc.sh
@@ -5,14 +5,17 @@ src=""
self=$(realpath $(which $0))
inst_dir=$(dirname $self)
+info=""
while [ "$1" != "" ]; do
a="$1"
shift
if [ "$a" = "-h" ]; then
- echo "extract_user_doc.sh"
- echo " ./scripts/extract_user_doc"
+ echo "./scripts/extract_user_doc -i "
exit 1
+ elif [ "$a" = "-i" ]; then
+ info="$1"
+ shift
else
echo "invalid option $a"
exit 1
@@ -20,6 +23,7 @@ while [ "$1" != "" ]; do
done
doc_src=./src/lay/lay/doc
+. ./version.sh
for qt in 5 4; do
@@ -50,7 +54,7 @@ for qt in 5 4; do
export KLAYOUT_HOME=$bin
rm -f $bin/help-index.xml
- $bin/klayout -rx -b -rd "target_doc=$target_doc" -rd "qt=$qt" -r $inst_dir/extract_user_doc.rb
+ $bin/klayout -rx -b -rd "target_doc=$target_doc" -rd "target_info=$info" -rd "qt=$qt" -r $inst_dir/extract_user_doc.rb
# just big:
# mv $bin/help-index.xml $target_doc/help-index.data