diff options
| author | Tristan Gingold <tgingold@free.fr> | 2018-04-13 19:35:42 +0200 |
|---|---|---|
| committer | Tristan Gingold <tgingold@free.fr> | 2018-04-13 19:35:42 +0200 |
| commit | ba14e9da2a0ca776e6be758f5b0fa49f6090e838 (patch) | |
| tree | 993bedec3728e6257f4f76359911c3392efd4a08 | |
| parent | 4d591aebdf4d855b47e519095cd9f2f10181459c (diff) | |
| download | ghdl-ba14e9da2a0ca776e6be758f5b0fa49f6090e838.tar.gz ghdl-ba14e9da2a0ca776e6be758f5b0fa49f6090e838.tar.bz2 ghdl-ba14e9da2a0ca776e6be758f5b0fa49f6090e838.zip | |
travis-ci.sh: call make with ghdl_version.
Tentative fix for #554
| -rwxr-xr-x | dist/linux/travis-ci.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dist/linux/travis-ci.sh b/dist/linux/travis-ci.sh index 51f7a83eb..2585685c8 100755 --- a/dist/linux/travis-ci.sh +++ b/dist/linux/travis-ci.sh @@ -100,7 +100,8 @@ else # This is a little bit hack-ish, as it assumes that 'git' is not # available in docker (otherwise it will describe as -dirty # because this modifies the source file version.in). - make -f Makefile.in srcdir=. version.tmp + ghdl_version_line=`grep -e '^ghdl_version' configure` + make -f Makefile.in srcdir=. $ghdl_version_line version.tmp cp version.tmp src/version.in # Run build in docker |