org: include the man pages in the generated userdoc
* doc/Makefile.am (org-man): New target. * tools/man2html.pl: Adjust to distinguish source and destination directories. Use relative links in genated files. * NEWS: Mention the html man pages.
This commit is contained in:
parent
f7b65001e9
commit
3897c8dc9a
3 changed files with 17 additions and 6 deletions
3
NEWS
3
NEWS
|
|
@ -3,6 +3,9 @@ New in spot 1.99.2a (not yet released)
|
||||||
* The CGI script for LTL translation offers a HOA download link
|
* The CGI script for LTL translation offers a HOA download link
|
||||||
for each generated automaton.
|
for each generated automaton.
|
||||||
|
|
||||||
|
* The html documentation now includes a HTML copies of the man
|
||||||
|
pages.
|
||||||
|
|
||||||
* Bugs fixed
|
* Bugs fixed
|
||||||
- Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
|
- Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
|
||||||
were not detected as generalized-Rabin.
|
were not detected as generalized-Rabin.
|
||||||
|
|
|
||||||
|
|
@ -49,12 +49,17 @@ $(srcdir)/spot.html $(srcdir)/spot.tag: $(srcdir)/stamp
|
||||||
# Spot documentation.
|
# Spot documentation.
|
||||||
dist_pkgdata_DATA = $(srcdir)/spot.tag
|
dist_pkgdata_DATA = $(srcdir)/spot.tag
|
||||||
|
|
||||||
.PHONY: org
|
.PHONY: org org-man
|
||||||
org:
|
org:
|
||||||
cd $(top_builddir) && $(MAKE) doc/org/init.el
|
cd $(top_builddir) && $(MAKE) doc/org/init.el
|
||||||
rm -rf $(srcdir)/userdoc
|
rm -rf $(srcdir)/userdoc
|
||||||
|
$(MAKE) org-man
|
||||||
$(EMACS) --batch -Q -l org/init.el
|
$(EMACS) --batch -Q -l org/init.el
|
||||||
|
|
||||||
|
org-man:
|
||||||
|
mkdir -p $(srcdir)/userdoc/man
|
||||||
|
$(top_srcdir)/tools/man2html.pl $(top_srcdir)/src/bin/man $(srcdir)/userdoc/man
|
||||||
|
|
||||||
ORG_FILES = \
|
ORG_FILES = \
|
||||||
org/.dir-locals.el.in \
|
org/.dir-locals.el.in \
|
||||||
org/g++wrap.in \
|
org/g++wrap.in \
|
||||||
|
|
|
||||||
|
|
@ -29,17 +29,20 @@ sub error($)
|
||||||
exit 1;
|
exit 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
error "Specify a directory with man pages\n" if @ARGV != 1;
|
error "Specify a directory with man pages and a directory for html pages\n"
|
||||||
|
if @ARGV != 2;
|
||||||
|
|
||||||
my $dir = @ARGV[0];
|
my $dir = @ARGV[0];
|
||||||
|
my $out = @ARGV[1];
|
||||||
|
|
||||||
opendir(DIR, $dir) or die $!;
|
opendir(DIR, $dir) or die $!;
|
||||||
while (my $file = readdir(DIR))
|
while (my $file = readdir(DIR))
|
||||||
{
|
{
|
||||||
next unless $file =~ m/\.\d$/;
|
next unless $file =~ m/\.\d$/;
|
||||||
|
my $ofile = "$out/$file.html";
|
||||||
$file = "$dir/$file";
|
$file = "$dir/$file";
|
||||||
print "converting $file to $file.html with groff\n";
|
print "converting $file to $ofile with groff\n";
|
||||||
my $html = `(echo '.HEAD <LINK REL="stylesheet" TYPE="text/css" HREF="https://spot.lrde.epita.fr/spot.css">'
|
my $html = `(echo '.HEAD <LINK REL="stylesheet" TYPE="text/css" HREF="../spot.css">'
|
||||||
echo '.HEAD <meta name="viewport" content="width=device-width, initial-scale=1">'
|
echo '.HEAD <meta name="viewport" content="width=device-width, initial-scale=1">'
|
||||||
cat $file) | groff -Kutf8 -mandoc -Thtml - -P -r`;
|
cat $file) | groff -Kutf8 -mandoc -Thtml - -P -r`;
|
||||||
$html =~ s|GNU GPL version 3 or later.*http://gnu.org/licenses/gpl.html>|<a href="http://gnu.org/licenses/gpl.html">GNU GPL version 3 or later</a>|s;
|
$html =~ s|GNU GPL version 3 or later.*http://gnu.org/licenses/gpl.html>|<a href="http://gnu.org/licenses/gpl.html">GNU GPL version 3 or later</a>|s;
|
||||||
|
|
@ -52,11 +55,11 @@ while (my $file = readdir(DIR))
|
||||||
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*<br>|<h3 style="margin-left:11%">$1</h3><p style="margin-left:11%"><b>|smg;
|
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*<br>|<h3 style="margin-left:11%">$1</h3><p style="margin-left:11%"><b>|smg;
|
||||||
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*</b>\s*<br>|<h3 style="margin-left:11%">$1</h3><p style="margin-left:11%">|smg;
|
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*</b>\s*<br>|<h3 style="margin-left:11%">$1</h3><p style="margin-left:11%">|smg;
|
||||||
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*</b></p>|<h3 style="margin-left:11%">$1</h3>|smg;
|
$html =~ s|<p style="margin-left:11%; margin-top: 1em"><b>([^<>]*?:)\s*</b></p>|<h3 style="margin-left:11%">$1</h3>|smg;
|
||||||
$html =~ s@<body>@<body class="man"><div id="org-div-home-and-up"><a accesskey="h" href="https://spot.lrde.epita.fr/tools.html"> UP </a>| <a accesskey="H" href="https://spot.lrde.epita.fr/index.html"> HOME </a></div>@;
|
$html =~ s@<body>@<body class="man"><div id="org-div-home-and-up"><a accesskey="h" href="../tools.html"> UP </a>| <a accesskey="H" href="../index.html"> HOME </a></div>@;
|
||||||
$html =~ s{<b>([\w-]+)</b>\((\d+)\)}{
|
$html =~ s{<b>([\w-]+)</b>\((\d+)\)}{
|
||||||
(-f "$1.$2") ? "<a href=\"$1.$2.html\"><b>$1</b></a>($2)" : $&;
|
(-f "$1.$2") ? "<a href=\"$1.$2.html\"><b>$1</b></a>($2)" : $&;
|
||||||
}xge;
|
}xge;
|
||||||
open(FILE, ">$file.html");
|
open(FILE, ">$ofile") or die $!;
|
||||||
print FILE $html;
|
print FILE $html;
|
||||||
close(FILE);
|
close(FILE);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue