mirror of
https://github.com/ralsina/tartrazine.git
synced 2025-05-23 16:40:08 -03:00
Merge pull request #126 from dpordomingo/shared-folder-rename
Rename .shared folder
This commit is contained in:
commit
c2ec7add03
1
.gitignore
vendored
1
.gitignore
vendored
@ -4,3 +4,4 @@ benchmarks/output
|
|||||||
Makefile.main
|
Makefile.main
|
||||||
.shared
|
.shared
|
||||||
.idea
|
.idea
|
||||||
|
.docsrv-resources
|
2
Makefile
2
Makefile
@ -15,7 +15,7 @@ $(MAKEFILE):
|
|||||||
LANGUAGES = go
|
LANGUAGES = go
|
||||||
# Docs: do not edit this
|
# Docs: do not edit this
|
||||||
DOCS_REPOSITORY := https://github.com/src-d/docs
|
DOCS_REPOSITORY := https://github.com/src-d/docs
|
||||||
SHARED_PATH ?= $(shell pwd)/.shared
|
SHARED_PATH ?= $(shell pwd)/.docsrv-resources
|
||||||
DOCS_PATH ?= $(SHARED_PATH)/.docs
|
DOCS_PATH ?= $(SHARED_PATH)/.docs
|
||||||
$(DOCS_PATH)/Makefile.inc:
|
$(DOCS_PATH)/Makefile.inc:
|
||||||
git clone --quiet --depth 1 $(DOCS_REPOSITORY) $(DOCS_PATH);
|
git clone --quiet --depth 1 $(DOCS_REPOSITORY) $(DOCS_PATH);
|
||||||
|
Loading…
x
Reference in New Issue
Block a user