feat(CMakeLists.txt): install *.md in standard/hott libraries
close #823
This commit is contained in:
parent
88739f0199
commit
f941af03ba
1 changed files with 3 additions and 5 deletions
|
@ -466,22 +466,20 @@ else()
|
||||||
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
|
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
|
||||||
endif()
|
endif()
|
||||||
|
|
||||||
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../library" DESTINATION "${LIBRARY_DIR}"
|
|
||||||
FILES_MATCHING PATTERN "*.lean")
|
|
||||||
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../library" DESTINATION "${LIBRARY_DIR}"
|
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../library" DESTINATION "${LIBRARY_DIR}"
|
||||||
FILES_MATCHING
|
FILES_MATCHING
|
||||||
PATTERN "*.lean"
|
PATTERN "*.lean"
|
||||||
PATTERN "*.olean"
|
PATTERN "*.olean"
|
||||||
PATTERN ".project"
|
PATTERN ".project"
|
||||||
|
PATTERN "*.md"
|
||||||
PATTERN "TAGS")
|
PATTERN "TAGS")
|
||||||
|
|
||||||
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../hott" DESTINATION "${LIBRARY_DIR}"
|
|
||||||
FILES_MATCHING PATTERN "*.hlean")
|
|
||||||
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../hott" DESTINATION "${LIBRARY_DIR}"
|
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../hott" DESTINATION "${LIBRARY_DIR}"
|
||||||
FILES_MATCHING
|
FILES_MATCHING
|
||||||
PATTERN "*.lean"
|
PATTERN "*.hlean"
|
||||||
PATTERN "*.olean"
|
PATTERN "*.olean"
|
||||||
PATTERN ".project"
|
PATTERN ".project"
|
||||||
|
PATTERN "*.md"
|
||||||
PATTERN "TAGS")
|
PATTERN "TAGS")
|
||||||
|
|
||||||
install(FILES "${CMAKE_SOURCE_DIR}/../src/emacs/lean.pgm"
|
install(FILES "${CMAKE_SOURCE_DIR}/../src/emacs/lean.pgm"
|
||||||
|
|
Loading…
Reference in a new issue