mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Merge pull request #2880 from nukisman/patch-3
Fix typo in custom backend cookbook: Phase --> UsePhase
This commit is contained in:
commit
249b0026d8
@ -120,7 +120,7 @@ Which Intermediate Representation (IR) should be consumed by the custom back-end
|
||||
|
||||
Now lets turn our attention to the different intermediate representations (IRs)
|
||||
that Idris provides.
|
||||
When the ``getCompileData`` function is invoked with the ``Phase`` parameter
|
||||
When the ``getCompileData`` function is invoked with the ``UsePhase`` parameter
|
||||
it will produce a ``CompileData`` record, which will contain lists of top-level
|
||||
definitions that needs to be compiled. These are:
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user