Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
e018a89f
Commit
e018a89f
authored
Jan 10, 2022
by
Michael Sammler
Browse files
add _opam to ignored directories for file check
parent
b4154715
Pipeline
#60746
failed with stage
in 15 minutes and 58 seconds
Changes
1
Pipelines
7
Hide whitespace changes
Inline
Side-by-side
frontend/main.ml
View file @
e018a89f
...
...
@@ -539,7 +539,7 @@ let init : string option -> unit = fun coq_path ->
panic
"File
\"
%s
\"
uses a reserved name."
path
else
()
in
Filename
.
iter_files
~
ignored_dirs
:
[
".git"
;
"_build"
]
wd
file_check
;
Filename
.
iter_files
~
ignored_dirs
:
[
".git"
;
"_build"
;
"_opam"
]
wd
file_check
;
(* Check for conflicting projects in parent directories. *)
let
rec
check_parents
dir
=
let
check_dir
dir
=
...
...
Michael Sammler
@msammler
mentioned in issue
#49 (closed)
·
Jan 10, 2022
mentioned in issue
#49 (closed)
mentioned in issue #49
Toggle commit list
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment