diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2019-04-30 10:50:30 +0200 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2019-04-30 10:50:30 +0200 |
| commit | 5dd0d1f8b3fc29d235eb25bb72a4b0d7160eba4d (patch) | |
| tree | 39c1cd04e658cecf210be044a358651aa8204a2b | |
| parent | d60225d5caabfb6409e3277c0512cd4c0fa63d72 (diff) | |
Revert "maint: 'release' clears gettext-induced changes in doc/."
This reverts commit 24963c13075b07db0c4e6005df9cde3bb51b2e32.
This change had become unnecessary since
9ca5ff882e2ac4eaab02eb0fde545bd784af478b.
| -rw-r--r-- | Makefile.am | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.am b/Makefile.am index 45807af8b89..deec100c3c0 100644 --- a/Makefile.am +++ b/Makefile.am | |||
| @@ -714,7 +714,6 @@ system_flags = $(foreach system,$(1),-s $(system)) | |||
| 714 | # issue described at <https://savannah.gnu.org/bugs/index.php?51027>. | 714 | # issue described at <https://savannah.gnu.org/bugs/index.php?51027>. |
| 715 | release: dist | 715 | release: dist |
| 716 | cd po; git checkout . | 716 | cd po; git checkout . |
| 717 | cd doc; git checkout . | ||
| 718 | @if ! git diff-index --quiet HEAD; then \ | 717 | @if ! git diff-index --quiet HEAD; then \ |
| 719 | echo "There are uncommitted changes; stopping." >&2 ; \ | 718 | echo "There are uncommitted changes; stopping." >&2 ; \ |
| 720 | exit 1 ; \ | 719 | exit 1 ; \ |