diff options
Diffstat (limited to 'Docs/Support/make-makefile')
| -rwxr-xr-x | Docs/Support/make-makefile | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Docs/Support/make-makefile b/Docs/Support/make-makefile new file mode 100755 index 00000000000..79cf06091fe --- /dev/null +++ b/Docs/Support/make-makefile @@ -0,0 +1,7 @@ +#!/bin/sh +# Use this when you have deleted Makefile and do not want to do a full +# build to get it back + +cd .. +automake --gnu Docs/Makefile +CONFIG_FILES=Docs/Makefile CONFIG_HEADERS= sh ./config.status |