Use spci_vcpu_index_t for vCPU indices.

Change-Id: Ia4817abcec05a3c46f0006274d0f6183bae69c3f
1 file changed
tree: fd84bf31cf25e68ceae3607b2ccc29942f09e7c3
  1. .gitignore
  2. AUTHORS
  3. LICENSE
  4. Makefile
  5. hf_call.S
  6. main.c