Skip to content

Commit d52438e

Browse files
committed
import
1 parent b409923 commit d52438e

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

‎Manual.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ import Manual.Releases
2929
import Manual.Namespaces
3030
import Manual.Runtime
3131
import Manual.ModuleSystem
32+
import Manual.Order.Test
3233

3334
open Verso.Genre Manual
3435
open Verso.Genre.Manual.InlineLean

0 commit comments

Comments
 (0)