merge the different manual/*.rst include files. Was too hard to find the corresponding sections otherwise. Hope it means the manual is more likely to be kept up to date.

This commit is contained in:
Andreas Rumpf 2018-04-14 08:42:45 +02:00
commit c6f15c53f4
25 changed files with 8057 additions and 8034 deletions

File diff suppressed because it is too large Load diff