diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Makefile b/src/Makefile index e2f063a2..09dfabc8 100644 --- a/src/Makefile +++ b/src/Makefile @@ -50,7 +50,7 @@ get_elf: cp -a $(ELFDIR)/src/abis/power64/*.ml src_elf/abis/power64 cp -a $(ELFDIR)/src/abis/aarch64/*.ml src_elf/abis/aarch64 cp -a $(ELFDIR)/src/adaptors/*.ml src_elf/adaptors - cp -a $(ELFDIR)/src/gnu_extensions/*.ml* + cp -a $(ELFDIR)/src/gnu_extensions/*.ml* src_elf/gnu_extensions chmod ugo-w src_elf/*.ml* chmod ugo-w src_elf/abis/*.ml* chmod ugo-w src_elf/abis/amd64/*.ml* |