Added a tip#172

Merged

vchuravy merged 2 commits intoJuliaCI:masterfrom

pauljurczak:patch-1

Jul 19, 2020

Commits on Jul 18, 2020

Added a tip
pauljurczak
authored

Commits on Jul 19, 2020

Update doc/manual.md

vchuravy
and
tpapp
authored