Opened 5 years ago

Closed 16 months ago

#23747 closed enhancement (invalid)

Rename SAGE_ROOT/build to SAGE_ROOT/sage-distro, SAGE_ROOT/src to SAGE_ROOT/sagelib

Reported by: Matthias Köppe Owned by:
Priority: major Milestone: sage-duplicate/invalid/wontfix
Component: build Keywords:
Cc: Volker Braun, Jeroen Demeyer, Travis Scrimshaw, Samuel Lelièvre Merged in:
Authors: Reviewers: Samuel Lelièvre
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges


I propose to rename build to sage-distro and src to sagelib (cf. #21507). This is to clarify the purpose of these directories.

Too many things are called src and build, even more with #21469 (VPATH), it's getting confusing.

I'm hoping git is smart enough to handle such renames when we merge tickets, but I am not sure.

Change History (3)

comment:1 Changed 20 months ago by Matthias Köppe

Dependencies: #31577
Milestone: sage-8.2sage-duplicate/invalid/wontfix
Status: newneeds_review

Superseded by #31577

comment:2 Changed 16 months ago by Samuel Lelièvre

Cc: Samuel Lelièvre added
Dependencies: #31577
Reviewers: Samuel Lelièvre
Status: needs_reviewpositive_review

Let us close this now that #31577 is in.

comment:3 Changed 16 months ago by Matthias Köppe

Resolution: invalid
Status: positive_reviewclosed
Note: See TracTickets for help on using tickets.