diff options
author | Michael Soegtrop <michael.soegtrop@intel.com> | 2018-06-15 18:57:00 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-25 16:37:02 +0200 |
commit | cb885e8c70a75043ff89e117c29cbb5dc22ff16f (patch) | |
tree | 9b9d84ef9f0b7151c33bb889493679e01aad92d6 /dev/build/windows/MakeCoq_MinGW.bat | |
parent | 915452f9a73d25e45131edb08531c29a79ab7020 (diff) |
Fix for issue 7707: include Ltac2 and Equations in Windows build
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
Diffstat (limited to 'dev/build/windows/MakeCoq_MinGW.bat')
-rwxr-xr-x[-rw-r--r--] | dev/build/windows/MakeCoq_MinGW.bat | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index f960ff008..5af0fcff3 100644..100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -255,6 +255,7 @@ IF NOT "%~0" == "" ( IF NOT EXIST %SETUP% ( ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html. + ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option. GOTO :EOF ) @@ -385,7 +386,6 @@ IF "%RUNSETUP%"=="Y" ( MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" ) - IF NOT "%CYGWIN_QUIET%" == "Y" ( REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it. REM This is not required with the -cygquiet=Y and the resulting --no-admin option. @@ -396,6 +396,12 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ========== +REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear +REM HOME (otherwise we get to the home directory of the other installation) +REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user) +SET "HOME=" +SET "PROFILEREAD=" + copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit |