author | Oleksandr Gavenko <gavenkoa@gmail.com> |
Mon, 19 Oct 2015 17:04:52 +0300 | |
changeset 1769 | cadd23f8127f |
parent 841 | a6d2c01cc279 |
permissions | -rw-r--r-- |
733 | 1 |
-*- mode: outline; coding: utf-8 -*- |
2 |
||
3 |
* Convert texi to html. |
|
4 |
||
5 |
** texi2html. |
|
6 |
||
7 |
http://www.mathematik.uni-kl.de/~obachman/Texi2html/ |
|
8 |
Texi2html's Homepage |
|
9 |
||
841
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
10 |
* Install texi files. |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
11 |
|
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
12 |
$ install -m 444 my.info.gz /usr/local/share/info |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
13 |
$ cd /usr/local/share/info |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
14 |
$ install-info --name=my --entry="My utilities." my.info.gz dir |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
15 |
|
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
16 |
For debug you can use '--dry-run' (do nothing). |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
17 |
|
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
18 |
* Uninstall texi files. |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
19 |
|
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
20 |
$ cd /usr/local/share/info |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
21 |
$ install-info --delete my.info.gz dir |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
22 |
$ rm my.info.gz |
a6d2c01cc279
Install/uninstall texi files.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
733
diff
changeset
|
23 |