Differences

This shows you the differences between two versions of the page.

--- install:install [2020/06/15 12:32] – flint and updates benmuell
+++ install:install [2020/06/15 12:34] – no docs build anymore benmuell
@@ Line 179: / Line 179: @@
 **Note:** If you are installing polymake in your home-directory, i.e. you have set ''%%--prefix%%'', you should omit ''sudo'' in the above commands.
-==== Building the documentation ====
-Finally, to obtain a copy of the reference documentation in HTML format (gathering everything you can get with interactive ''help'' commands a one place), run
-  sudo make release-docs
-This will create all files in the documentation directory chosen during the configuration, again omit sudo for a user-install. By default the documentation will be installed into ''/usr/local/share/polymake/doc''.
-If you have already used polymake and installed extensions to polymake then to include them for the documentation, run
-  sudo make docs
-Should you import or create a new extension later, you can also run the polymake script ''generate_docs'' to complete your documentation.
 ===== Dependency lists for common distros =====