diff options
| author | Robert Pluim | 2018-03-22 09:06:44 +0100 |
|---|---|---|
| committer | Robert Pluim | 2018-03-23 09:15:42 +0100 |
| commit | 31ce174a7228499eb2264e701fd8d16bd291c25f (patch) | |
| tree | cfc98fa7e853038c1de2c4cf51817a01d27d0903 /admin/update_autogen | |
| parent | dfea6d5a4aac5fd1679a917c5e84ce17a6c6a3d8 (diff) | |
| download | emacs-31ce174a7228499eb2264e701fd8d16bd291c25f.tar.gz emacs-31ce174a7228499eb2264e701fd8d16bd291c25f.zip | |
Make update_autogen work in git worktrees
* admin/update_autogen: Make it work in a git worktree
Diffstat (limited to 'admin/update_autogen')
| -rwxr-xr-x | admin/update_autogen | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/admin/update_autogen b/admin/update_autogen index d2118674792..f4c2c39825c 100755 --- a/admin/update_autogen +++ b/admin/update_autogen | |||
| @@ -47,7 +47,7 @@ cd $PD | |||
| 47 | cd ../ | 47 | cd ../ |
| 48 | [ -d admin ] || die "Could not locate admin directory" | 48 | [ -d admin ] || die "Could not locate admin directory" |
| 49 | 49 | ||
| 50 | [ -d .git ] || die "No .git directory" | 50 | [ -d .git ] || git rev-parse --git-dir > /dev/null 2>&1 || die "Not in a git repository" |
| 51 | 51 | ||
| 52 | usage () | 52 | usage () |
| 53 | { | 53 | { |