diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2016-10-11 12:25:42 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-10-11 12:25:42 +0200 |
| commit | fb1dbba5e35d1fc7c00250f597b8c796d8c96eda (patch) | |
| tree | 908168d0edf0077b99e9bd7cc656787a03198d0e /docs/docs | |
| parent | 618cebbec6fd5727b51974fa372ae984c03f9f99 (diff) | |
| parent | 2f252a483bf4e74b1660957a69d108c23fb2c88a (diff) | |
| download | dotty-fb1dbba5e35d1fc7c00250f597b8c796d8c96eda.tar.gz dotty-fb1dbba5e35d1fc7c00250f597b8c796d8c96eda.tar.bz2 dotty-fb1dbba5e35d1fc7c00250f597b8c796d8c96eda.zip | |
Merge pull request #1578 from MasseGuillaume/topic/use-env
use usr/bin/env bash since it's more general then /bin/bash
Diffstat (limited to 'docs/docs')
0 files changed, 0 insertions, 0 deletions