diff options
| author | Pierre-Marie Pédrot | 2018-05-26 20:20:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-26 20:20:33 +0200 |
| commit | 71557d5499fcf78d023eefc8d7a2b7a118b81ed5 (patch) | |
| tree | a54a50a8b7758823709ee776b4825702e3003dcf /ide/protocol/ideprotocol.mllib | |
| parent | ac2c4bc19afe7d68918cbc6f605a9bcfcdbf0f35 (diff) | |
| parent | 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (diff) | |
Merge PR #7543: [ide] Move common protocol library to its own folder/object.
Diffstat (limited to 'ide/protocol/ideprotocol.mllib')
| -rw-r--r-- | ide/protocol/ideprotocol.mllib | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib new file mode 100644 index 0000000000..8317a08681 --- /dev/null +++ b/ide/protocol/ideprotocol.mllib @@ -0,0 +1,7 @@ +Xml_lexer +Xml_parser +Xml_printer +Serialize +Richpp +Interface +Xmlprotocol |