Feedback: File Dependencies - siegebell/vscoq GitHub Wiki

Typically emitted in response to a Require. Dependencies are *.vo files.

Format:

  • State stateId directly depends on dependency:
<feedback object="state" route="0">
  <state_id val="${stateId}"/>
  <feedback_content val="filedependency">
    <option val="none"/>
    <string>${dependency}</string>
  </feedback_content>
</feedback>
  • State stateId depends on dependency via dependency sourceDependency
<feedback object="state" route="0">
  <state_id val="${stateId}"/>
  <feedback_content val="filedependency">
    <option val="some"><string>${sourceDependency}</string></option>
    <string>${dependency}</string>
  </feedback_content>
</feedback>
⚠️ **GitHub.com Fallback** ⚠️