diff options
| author | Damien Doligez <damien.doligez@inria.fr> | 2015-11-20 17:54:26 +0100 |
|---|---|---|
| committer | Damien Doligez <damien.doligez@inria.fr> | 2015-12-21 14:27:46 +0100 |
| commit | 0225ca01e39289ce1801fb09cd011cdbfb542b8d (patch) | |
| tree | 378687ce2803504471b133900b9bf24d5afa0950 /tools/Makefile.shared | |
| parent | 7c71653524ccb922b78456209e0f5c47573db5e9 (diff) | |
| download | ocaml-0225ca01e39289ce1801fb09cd011cdbfb542b8d.tar.gz | |
GC latency improvements
Diffstat (limited to 'tools/Makefile.shared')
| -rw-r--r-- | tools/Makefile.shared | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/Makefile.shared b/tools/Makefile.shared index 1761d30866..7bbbc46516 100644 --- a/tools/Makefile.shared +++ b/tools/Makefile.shared @@ -312,6 +312,11 @@ cmpbyt: $(CMPBYT) clean:: rm -f cmpbyt +ifeq "$(RUNTIMEI)" "true" +install:: + cp ocaml-instr-graph ocaml-instr-report $(INSTALL_BINDIR)/ +endif + # Common stuff .SUFFIXES: |