diff options
| author | Paul Steckler | 2017-04-27 12:05:51 -0400 |
|---|---|---|
| committer | Paul Steckler | 2017-04-27 12:05:51 -0400 |
| commit | e574b4bdd974daa7d2ceecf799762be92fadff44 (patch) | |
| tree | a4fd54fedd13150bd30cedd1778634bb2344af9b /pretyping/patternops.ml | |
| parent | 746066172b8ed508886feb20cee239920ca7a4c7 (diff) | |
fix order of command-line arguments mentioned in Add LoadPath
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions