diff options
| author | Richard W.M. Jones <rjones@redhat.com> | 2008-03-19 11:34:00 +0000 |
|---|---|---|
| committer | Richard W.M. Jones <rjones@redhat.com> | 2008-03-19 11:34:00 +0000 |
| commit | 6d1e1917a4c8ae136276c3c308d563d4940c982a (patch) | |
| tree | dfcb55bea2e22be4f54662b80b5731e93ee3f47c /virt-ctrl/virt_ctrl.ml | |
| parent | 3100a9fc683b327a154a04266bb1ec0efc349f00 (diff) | |
Install the *.cmi files as well.
Diffstat (limited to 'virt-ctrl/virt_ctrl.ml')
0 files changed, 0 insertions, 0 deletions