diff options
author | Son Ho | 2023-01-24 00:09:33 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | a9110a7fe013dc7b6dd35bfd6f56ea1ce3a471b1 (patch) | |
tree | c08dbb5ea6b8620562f9503bf9a4241d8bf6be0e /backends/hol4/Holmakefile | |
parent | 8ab6291e717a1ad0fe77dcabca928491134708e3 (diff) |
Make minor modifications
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/Holmakefile | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backends/hol4/Holmakefile b/backends/hol4/Holmakefile index 49cc6da7..3e5606fb 100644 --- a/backends/hol4/Holmakefile +++ b/backends/hol4/Holmakefile @@ -2,8 +2,3 @@ INCLUDES = all: $(DEFAULT_TARGETS) .PHONY: all - -README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) -DIRS = $(wildcard */) -README.md: $(README_SOURCES) - $(README_SOURCES) |