diff options
| author |  Benjamin Jones <bjones@galois.com> | 2013-02-21 17:48:28 -0800 |
|---|---|---|
| committer | Benjamin Jones <bjones@galois.com> | 2013-02-21 17:48:28 -0800 |
| commit | e6132af29e23e398848e0607522864e7713ebc05 (patch) | |
| tree | bf9f2644d13192bfa2f00b59ce7ce59a8a4ce872 /Makefile | |
| parent | 31bb8e63b2c4d2d67c953622517ba786c1019a9c (diff) | |
added install target to Makefile that moves extension binaries to FIVEUI_ROOT/binaries
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions