Admin/Cygwin/Cygwin-Terminal.bat
author wenzelm
Mon, 23 Apr 2012 23:38:35 +0200
changeset 47708 49c05c666475
child 47721 77d9881bc820
permissions -rwxr-xr-x
basic Cygwin-Terminal for main Isabelle directory;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47708
49c05c666475 basic Cygwin-Terminal for main Isabelle directory;
wenzelm
parents:
diff changeset
     1
@echo off
49c05c666475 basic Cygwin-Terminal for main Isabelle directory;
wenzelm
parents:
diff changeset
     2
49c05c666475 basic Cygwin-Terminal for main Isabelle directory;
wenzelm
parents:
diff changeset
     3
set HOME=%HOMEDRIVE%%HOMEPATH%
49c05c666475 basic Cygwin-Terminal for main Isabelle directory;
wenzelm
parents:
diff changeset
     4
set PATH=%CD%\bin;%PATH%
49c05c666475 basic Cygwin-Terminal for main Isabelle directory;
wenzelm
parents:
diff changeset
     5
"%CD%\contrib\cygwin-1.7.9\bin\bash" --login -i