diff options
author | 1138-4EB <1138-4EB@users.noreply.github.com> | 2019-08-31 17:32:35 +0200 |
---|---|---|
committer | tgingold <tgingold@users.noreply.github.com> | 2019-08-31 17:32:35 +0200 |
commit | b124c3926b05d7d0770989330039518c391f73cf (patch) | |
tree | ff417a3940604ca8be2f005ae0d93302afcd4519 /doc/_extensions | |
parent | 6852a8f2b79f87ffb523f0aa4157f23540818887 (diff) | |
download | ghdl-b124c3926b05d7d0770989330039518c391f73cf.tar.gz ghdl-b124c3926b05d7d0770989330039518c391f73cf.tar.bz2 ghdl-b124c3926b05d7d0770989330039518c391f73cf.zip |
[doc] Update section 'Getting GHDL' (#906)
* doc: fix version extraction from 'configure'
* doc: update section 'Getting GHDL'
* readme: update
Diffstat (limited to 'doc/_extensions')
-rw-r--r-- | doc/_extensions/.gitempty | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/_extensions/.gitempty b/doc/_extensions/.gitempty deleted file mode 100644 index e69de29bb..000000000 --- a/doc/_extensions/.gitempty +++ /dev/null |